Merge pull request #1033 from MetaCoq/primitive-flags

Primitive flags
MetaCoq · Dec 22, 2023 · c36b24b · c36b24b
2 parents e9b17dc + f526608
commit c36b24b
Show file tree

Hide file tree

Showing 15 changed files with 386 additions and 338 deletions.
diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v
@@ -87,6 +87,7 @@ Section transform_blocks.
 
   End Def.
 
+  #[universes(polymorphic)]
   Hint Rewrite @map_primIn_spec @map_InP_spec : transform_blocks.
 
   Arguments eqb : simpl never.
@@ -428,6 +429,7 @@ Section transform_blocks.
 
 End transform_blocks.
 
+#[universes(polymorphic)]
 Global Hint Rewrite @map_primIn_spec @map_InP_spec : transform_blocks.
 
 Definition transform_blocks_constant_decl Σ cb :=

diff --git a/erasure/theories/EEtaExpanded.v b/erasure/theories/EEtaExpanded.v
@@ -100,6 +100,7 @@ Section isEtaExp.
 
 End isEtaExp.
 
+#[universes(polymorphic)]
 Global Hint Rewrite @test_primIn_spec @forallb_InP_spec : isEtaExp.
 Tactic Notation "simp_eta" "in" hyp(H) := simp isEtaExp in H; rewrite -?isEtaExp_equation_1 in H.
 Ltac simp_eta := simp isEtaExp; rewrite -?isEtaExp_equation_1.

diff --git a/erasure/theories/EEtaExpandedFix.v b/erasure/theories/EEtaExpandedFix.v
@@ -334,7 +334,7 @@ Section isEtaExp.
   Qed.
 
   Hint Rewrite @forallb_InP_spec : isEtaExp.
-  Hint Rewrite @test_primIn_spec : isEtaExp.
+  #[universes(polymorphic)] Hint Rewrite @test_primIn_spec : isEtaExp.
 
   Lemma isEtaExp_mkApps_nonnil Γ f v :
     ~~ isApp f -> v <> [] ->
@@ -773,7 +773,7 @@ Section isEtaExp.
 
 End isEtaExp.
 Global Hint Rewrite @forallb_InP_spec : isEtaExp.
-Global Hint Rewrite @test_primIn_spec : isEtaExp.
+#[universes(polymorphic)] Global Hint Rewrite @test_primIn_spec : isEtaExp.
 
 Tactic Notation "simp_eta" "in" hyp(H) := simp isEtaExp in H; rewrite -?isEtaExp_equation_1 in H.
 Ltac simp_eta := simp isEtaExp; rewrite -?isEtaExp_equation_1.

diff --git a/erasure/theories/EImplementBox.v b/erasure/theories/EImplementBox.v
@@ -67,6 +67,7 @@ Section implement_box.
 
   End Def.
 
+  #[universes(polymorphic)]
   Hint Rewrite @map_primIn_spec @map_InP_spec : implement_box.
 
   Arguments eqb : simpl never.
@@ -265,6 +266,7 @@ Section implement_box.
 
 End implement_box.
 
+#[universes(polymorphic)]
 Global Hint Rewrite @map_primIn_spec @map_InP_spec : implement_box.
 
 Definition implement_box_constant_decl cb :=
@@ -670,7 +672,7 @@ Proof.
     rewrite lookup_constructor_implement_box; eauto.
     eapply All2_All2_Set.
     solve_all. now destruct b.
-  - intros H; depelim H; simp implement_box; repeat constructor.
+  - intros wf H; depelim H; simp implement_box; repeat constructor.
     destruct a0. eapply All2_over_undep in a. eapply All2_All2_Set, All2_map.
     cbn -[implement_box]. solve_all. now destruct H. now destruct a0.
   - intros. destruct t; try solve [constructor; cbn in H, H0 |- *; try congruence].

diff --git a/erasure/theories/EInlineProjections.v b/erasure/theories/EInlineProjections.v
@@ -166,7 +166,7 @@ Section optimize.
     - len. rtoProp; solve_all. solve_all.
       now eapply isLambda_optimize. solve_all.
     - len. rtoProp; repeat solve_all.
-    - rewrite test_prim_map. solve_all.
+    - rewrite test_prim_map. rtoProp; intuition eauto; solve_all.
   Qed.
 
   Lemma optimize_csubst {a k b} n :
@@ -716,11 +716,12 @@ Proof.
         rewrite optimize_mkApps !isConstructApp_mkApps !isPrimApp_mkApps.
         destruct args using rev_case => // /=. rewrite map_app !mkApps_app /= //.
         destruct v => /= //.
-  - depelim X; repeat constructor.
+  - intros; rtoProp; intuition eauto.
+    depelim X; repeat constructor.
     eapply All2_over_undep in a.
     eapply All2_Set_All2 in ev. eapply All2_All2_Set. primProp.
-    subst a0 a'; cbn in *. depelim H; cbn in *. intuition auto; solve_all.
-    primProp; depelim H; intuition eauto.
+    subst a0 a'; cbn in *. depelim H0; cbn in *. intuition auto; solve_all.
+    primProp; depelim H0; intuition eauto.
   - destruct t => //.
     all:constructor; eauto.
     cbn [atom optimize] in i |- *.