From 7de5f9099dbf27e84110a1ed2923e66f62d10e82 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Thu, 5 Jan 2017 13:59:22 +0100
Subject: [PATCH] Fix build by implementing th things I forgot.
---
theories/typing/cont_context.v | 16 +++++++++++++++-
theories/typing/function.v | 1 -
theories/typing/lft_contexts.v | 2 +-
theories/typing/product.v | 1 -
theories/typing/sum.v | 1 -
5 files changed, 16 insertions(+), 5 deletions(-)
diff --git a/theories/typing/cont_context.v b/theories/typing/cont_context.v
index b403d833..b77593cc 100644
--- a/theories/typing/cont_context.v
+++ b/theories/typing/cont_context.v
@@ -92,7 +92,7 @@ Section cont_context.
iApply ("H" with "HE * [%]"). by apply HC1C2.
Qed.
- Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
+ Lemma cctx_incl_cons_match E k L n (T1 T2 : vec val n → tctx) C1 C2 :
cctx_incl E C1 C2 → (∀ args, tctx_incl E L (T2 args) (T1 args)) →
cctx_incl E (k â—cont(L, T1) :: C1) (k â—cont(L, T2) :: C2).
Proof.
@@ -111,4 +111,18 @@ Section cont_context.
Lemma cctx_incl_nil E C : cctx_incl E C [].
Proof. apply incl_cctx_incl. by set_unfold. Qed.
+ Lemma cctx_incl_cons E k L n (T1 T2 : vec val n → tctx) C1 C2 :
+ (k â—cont(L, T1))%CC ∈ C1 →
+ (∀ args, tctx_incl E L (T2 args) (T1 args)) →
+ cctx_incl E C1 C2 →
+ cctx_incl E C1 (k â—cont(L, T2) :: C2).
+ Proof.
+ intros Hin ??. rewrite <-cctx_incl_cons_match; try done.
+ iIntros (??) "_ HC HE". iSpecialize ("HC" with "HE").
+ rewrite cctx_interp_cons. iSplit; last done. clear -Hin.
+ iInduction Hin as [] "IH"; rewrite cctx_interp_cons;
+ [iDestruct "HC" as "[$ _]" | iApply "IH"; iDestruct "HC" as "[_ $]"].
+ Qed.
End cont_context.
+
+Hint Resolve cctx_incl_nil cctx_incl_cons : lrust_typing.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index fdcb02f4..c649ca84 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -268,4 +268,3 @@ Section typing.
End typing.
Hint Resolve fn_subtype_full : lrust_typing.
-Hint Constructors Forall2 elem_of_list: lrust_typing.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index a6a66266..486b54bf 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -424,7 +424,7 @@ End elctx_incl.
Ltac solve_typing := by eauto 100 with lrust_typing.
-Hint Constructors Forall : lrust_typing.
+Hint Constructors Forall Forall2 : lrust_typing.
Hint Resolve
lctx_lft_incl_relf lctx_lft_incl_static lctx_lft_incl_local'
lctx_lft_incl_external'
diff --git a/theories/typing/product.v b/theories/typing/product.v
index dbb855ff..58063ec6 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -246,5 +246,4 @@ End typing.
Hint Resolve product_mono' product_proper' : lrust_typing.
-Hint Constructors Forall2 : lrust_typing.
Hint Resolve product2_mono' product2_proper' | 100 : lrust_typing.
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index 79bee07a..6cb8c72a 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -238,4 +238,3 @@ Notation "Σ[ ty1 ; .. ; tyn ]" :=
(sum (cons ty1 (..(cons tyn nil)..))) : lrust_typing.
Hint Resolve sum_mono' sum_proper' : lrust_typing.
-Hint Constructors Forall2 : lrust_typing.
--
GitLab