Make scripts more robust when using simp and solving the goal trivially.

MetaCoq · May 23, 2024 · d6e0f45 · d6e0f45
1 parent d1f8f55
commit d6e0f45
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git a/erasure/theories/EEtaExpanded.v b/erasure/theories/EEtaExpanded.v
@@ -719,7 +719,7 @@ Proof.
     solve_all.
   - eapply In_All in H. simp_eta.
     move=> /andP[] etarel etav.
-    eapply EEtaExpanded.isEtaExp_mkApps_intro. simp_eta. solve_all.
+    eapply EEtaExpanded.isEtaExp_mkApps_intro. now simp_eta. solve_all.
   - eapply In_All in H0. simp_eta.
     move=> /andP[] etau etav.
     eapply EEtaExpanded.isEtaExp_mkApps_intro; auto. solve_all.

diff --git a/erasure/theories/Typed/OptimizeCorrectness.v b/erasure/theories/Typed/OptimizeCorrectness.v
@@ -3191,7 +3191,7 @@ Proof.
     now eapply (isEtaExp_lift _ _ [_] []).
     eapply IHm; eauto. now move/andP: etal.
     eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]).
-    now eapply (isEtaExp_lift _ _ [_] []). constructor; eauto. simp_eta.
+    now eapply (isEtaExp_lift _ _ [_] []). constructor; eauto. now simp_eta.
     eapply IHm. eapply (isEtaExp_mkApps_intro _ _ _ [_]); eauto. constructor; eauto.
     all:now move/andP: etal.
 Qed.

diff --git a/pcuic/theories/PCUICParallelReductionConfluence.v b/pcuic/theories/PCUICParallelReductionConfluence.v
@@ -1785,7 +1785,7 @@ Section Rho.
           erewrite H; trea.
         + simp rho. simpl. f_equal; eauto.
           erewrite -> rho_rename_pred; tea => //.
-          simp rho.
+          now simp rho.
         + simp rho. simpl. simp rho. f_equal; eauto.
           erewrite -> rho_rename_pred; tea => //.
 
@@ -1850,7 +1850,8 @@ Section Rho.
         simp rho. simpl.
         f_equal; auto.
         erewrite rho_rename_pred; tea=> //.
-        now rewrite !map_map_compose in H0. simp rho.
+        now rewrite !map_map_compose in H0.
+        now simp rho.
 
     - (* Proj construct/cofix reduction *)
       simpl.