Fixes after rebase

MetaCoq · Nov 24, 2023 · 133b5ad · 133b5ad
1 parent 8b4d7a9
commit 133b5ad
Show file tree

Hide file tree

Showing 7 changed files with 14 additions and 12 deletions.
diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v
@@ -94,11 +94,11 @@ Section implement_box.
     rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length;
     unfold test_def in *;
     simpl closed in *;
-    (*try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy.
+    try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all]; try easy.
     rtoProp. split. eauto.
     solve_all.
     replace (#|x.1| + S k) with (#|x.1| + k + 1) by lia.
-    eapply closedn_lift. eauto.*)
+    eapply closedn_lift. eauto.
     try solve [simpl; subst; simpl closed; f_equal; auto; rtoProp; solve_all; solve_all_k 6]; try easy.
   Qed.
 
@@ -124,10 +124,9 @@ Section implement_box.
       f_equal. lia.
     - cbn. f_equal. rewrite !map_map. solve_all.
       eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto.
-      f_equal. now rewrite map_length.
     - cbn. f_equal. rewrite !map_map. solve_all.
       eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. erewrite H; eauto.
-      f_equal. now rewrite map_length.
+    - solve_all_k 6.
   Qed.
 
   (* Lemma implement_box_subst a k b : *)
@@ -185,9 +184,9 @@ Section implement_box.
       f_equal.
       eapply H; eauto.
     - cbn. f_equal. rewrite !map_map. solve_all.
-      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. solve_all.
     - cbn. f_equal. rewrite !map_map. solve_all.
-      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. rewrite H; eauto.
+      eapply In_All. intros ? ?. unfold map_def. cbn. f_equal. solve_all.
     - cbn. solve_all.
   Qed.
 

diff --git a/erasure/theories/EInduction.v b/erasure/theories/EInduction.v
@@ -67,7 +67,7 @@ Proof.
   destruct mfix; constructor; [|apply auxm].
   apply auxt.
 
-  destruct p as [? []]; cbn => //; constructor.
+  destruct prim as [? []]; cbn => //; constructor.
   destruct a as [def v]; cbn.
   split. eapply auxt.
   revert v; fix auxv 1.

diff --git a/erasure/theories/EReflect.v b/erasure/theories/EReflect.v
@@ -112,13 +112,13 @@ Proof.
         subst. inversion e0. subst.
         destruct (eq_dec rarg rarg0) ; nodec.
         subst. left. reflexivity.
-  - destruct p as [? []]; destruct p0 as [? []]; cbn ; nodec.
+  - destruct prim as [? []]; destruct p as [? []]; cbn ; nodec.
     + destruct (eq_dec i i0); nodec; subst; eauto.
     + destruct (eq_dec f f0); nodec; subst; eauto.
     + destruct a as [? ?], a0 as [? ?]; cbn.
       depelim X. destruct p as [hd hv]. cbn in *.
-      destruct (hd array_default0); nodec; subst; eauto.
-      revert array_value0; induction hv; intros []; eauto; nodec.
+      destruct (hd array_default); nodec; subst; eauto.
+      revert array_value; induction hv; intros []; eauto; nodec.
       destruct (p t); subst; nodec.
       destruct (IHhv l0); nodec. noconf e; eauto.
 Defined.

diff --git a/quotation/theories/CommonUtils.v b/quotation/theories/CommonUtils.v
@@ -188,6 +188,7 @@ Module WithTemplate.
          | tVar _
          | tInt _
          | tFloat _
+         | tArray _ _ _ _
          | tConst _ _
          | tInd _ _
          | tConstruct _ _ _

diff --git a/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v b/quotation/theories/ToPCUIC/QuotationOf/Common/Environment/Sig.v
@@ -43,7 +43,7 @@ Module Type QuoteEnvironmentSig (T : Term) (Import E : EnvironmentSig T).
 
   #[export] Declare Instance quote_extends {Σ Σ'} : ground_quotable (@extends Σ Σ').
   #[export] Declare Instance quote_extends_decls {Σ Σ'} : ground_quotable (@extends_decls Σ Σ').
-  #[export] Declare Instance quote_primitive_invariants {cdecl} : ground_quotable (primitive_invariants cdecl).
+  #[export] Declare Instance quote_primitive_invariants {cdecl ty} : ground_quotable (primitive_invariants cdecl ty).
 
   #[export] Declare Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t').
   #[export] Declare Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t').

diff --git a/quotation/theories/ToTemplate/Init.v b/quotation/theories/ToTemplate/Init.v
@@ -108,6 +108,7 @@ Proof.
      | tSort _
      | tInt _
      | tFloat _
+     | tArray _ _ _ _
      | tConst _ _
        => if head_term_is_bound cur_modpath qt
           then tmMaybeInferQuotation tt
@@ -212,6 +213,7 @@ Proof.
        | tConstruct _ _ _
        | tInt _
        | tFloat _
+       | tArray _ _ _ _
        | tInd _ _
          => ret qt
        | tCast t kind v

diff --git a/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v b/quotation/theories/ToTemplate/QuotationOf/Common/Environment/Sig.v
@@ -43,7 +43,7 @@ Module Type QuoteEnvironmentSig (T : Term) (Import E : EnvironmentSig T).
 
   #[export] Declare Instance quote_extends {Σ Σ'} : ground_quotable (@extends Σ Σ').
   #[export] Declare Instance quote_extends_decls {Σ Σ'} : ground_quotable (@extends_decls Σ Σ').
-  #[export] Declare Instance quote_primitive_invariants {cdecl} : ground_quotable (primitive_invariants cdecl).
+  #[export] Declare Instance quote_primitive_invariants {cdecl ty} : ground_quotable (primitive_invariants cdecl ty).
 
   #[export] Declare Instance quote_All_decls {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls P t t').
   #[export] Declare Instance quote_All_decls_alpha {P t t'} {qP : quotation_of P} {quoteP : forall t t', ground_quotable (P t t')} : ground_quotable (All_decls_alpha P t t').