Backward compatible fixes for update of equations funelim tactic bugfix.

erasure/theories/EConstructorsAsBlocks.v

@@ -729,7 +729,8 @@ Proof.
     eapply isEtaExp_mkApps in H1. rewrite decompose_app_mkApps in H1; eauto.
     destruct construct_viewc; eauto. cbn in d. eauto.
     split; rtoProp; intuition eauto. solve_all; intuition eauto.
-  - Opaque isEtaExp. destruct chop eqn:Ec. rewrite !wellformed_mkApps in Hw |- * => //. rtoProp.
+  - Opaque isEtaExp. try clear Heqcall. destruct chop eqn:Ec.
+    rewrite !wellformed_mkApps in Hw |- * => //. rtoProp.
     rewrite GlobalContextMap.lookup_constructor_pars_args_spec in Heq.
     cbn -[lookup_constructor transform_blocks ] in *. rewrite cstrbl in H1.
     rewrite lookup_constructor_transform_blocks. intros. rtoProp.
@@ -807,7 +808,7 @@ Proof.
   - f_equal. eauto. rewrite wellformed_mkApps in H1 => //. rtoProp.
     rewrite transform_blocks_mkApps; eauto. destruct construct_viewc; cbn in d; eauto.
     f_equal. eapply H; eauto. solve_all.
-  - destruct chop eqn:E.
+  - try clear Heqcall. destruct chop eqn:E.
     rewrite GlobalContextMap.lookup_constructor_pars_args_spec in Heq.
     rewrite wellformed_mkApps in H0 => //. rewrite transform_blocks_mkApps => //.
     rtoProp. cbn [construct_viewc]. unfold lookup_constructor_pars_args in *.

erasure/theories/EEtaExpandedFix.v

@@ -445,8 +445,8 @@ Section isEtaExp.
   Proof.
     funelim (isEtaExp Γ t); simp_eta; eauto; intros Hexp; toAll; solve_all; rtoProp; repeat solve_all; eauto.
     - destruct nth_error eqn:E; try easy. erewrite nth_error_app_left; eauto.
-    - rewrite app_assoc. eapply a, b. reflexivity.
-    - rewrite app_assoc. eapply a, b. reflexivity.
+    - rewrite app_assoc. eapply a, b; reflexivity.
+    - rewrite app_assoc. eapply a, b; reflexivity.
     - rewrite isEtaExp_mkApps => //. cbn [expanded_head_viewc]. rtoProp; repeat solve_all.
     - rewrite isEtaExp_mkApps => //. cbn [expanded_head_viewc]. rtoProp; repeat solve_all.
       rewrite app_assoc. rtoProp; intuition auto.
@@ -463,10 +463,12 @@ Section isEtaExp.
     - destruct nth_error eqn:Hn; cbn in H; try easy.
       eapply nth_error_Some_length in Hn. now eapply Nat.ltb_lt.
     - destruct block_args; cbn in *; eauto.
-    - eapply a in b. 2: f_equal. revert b. now len.
-    - eapply a in b. 2: f_equal. revert b. now len.
+    - (eapply a in b; [|f_equal]; revert b; now len) || (revert H; now len).
+    - (eapply a in b; [|f_equal]; revert b; now len) || (destruct x; cbn; revert H; now len).
     - cbn. destruct block_args; cbn in *; eauto.
-    - cbn. solve_all. rtoProp; intuition auto. eapply a in H0. 2: reflexivity. revert H0. now len.
+    - cbn. solve_all. rtoProp; intuition auto.
+      (eapply a in H0; [|reflexivity]; revert H0; now len) ||
+      (destruct x; cbn; revert H2; now len).
     - destruct nth_error eqn:Hn; cbn in H1; try easy.
       eapply nth_error_Some_length in Hn. now eapply Nat.ltb_lt.
   Qed.
@@ -1993,7 +1995,7 @@ Qed.
 
 Lemma isEtaExp_lift Σ Γ Γ' Γ'' t : isEtaExp Σ (Γ'' ++ Γ) t -> isEtaExp Σ (Γ'' ++ Γ' ++ Γ) (lift #|Γ'| #|Γ''| t).
 Proof using.
-  funelim (isEtaExp Σ _ t); cbn; simp_eta; try now easy; intros; solve_all.
+  funelim_nosimp (isEtaExp Σ _ t); cbn; simp_eta; try now easy; intros; solve_all.
   all:cbn; simp_eta; toAll; bool; try rewrite -> forallb_InP_spec in *.
   all:try solve [solve_all].
 

erasure/theories/ERemoveParams.v

@@ -1087,8 +1087,7 @@ Proof.
     rewrite lookup_env_strip. cbn in H1. destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g.
     destruct nth_error => //. rtoProp; intuition auto.
-    simp_strip. toAll; solve_all.
-    toAll. solve_all.
+    simp_strip. all:toAll; solve_all.
   - cbn -[strip] in H0 |- *.
     rewrite lookup_env_strip. destruct lookup_env eqn:hl => // /=.
     destruct g eqn:hg => /= //. subst g. cbn in H0. now rtoProp.
@@ -1100,7 +1099,7 @@ Proof.
     now rewrite -strip_isLambda. toAll; solve_all.
   - primProp. rtoProp; intuition eauto; solve_all_k 6.
   - move:H1; rewrite !wellformed_mkApps //. rtoProp; intuition auto.
-    toAll; solve_all. toAll; solve_all.
+    all:toAll; solve_all.
   - move:H0; rewrite !wellformed_mkApps //. rtoProp; intuition auto.
     move: H1. cbn. rewrite cab.
     rewrite lookup_env_strip. destruct lookup_env eqn:hl => // /=.

erasure/theories/ErasureFunction.v

@@ -926,14 +926,14 @@ Proof.
   - destruct type_of_typing as [x Hx]. cbn -[sort_of_type is_arity] in *.
     destruct (sort_of_type _ _ _ _). cbn.
     destruct (Sort.is_propositional x0) eqn:isp; constructor.
-    * clear Heq. intros.
+    * clear Heq; try clear Heqcall. intros.
       pose proof (abstract_env_ext_wf _ H) as [wf].
       specialize_Σ H.
       destruct Hx as [[HT ?]].
       destruct s as [Hs]. sq.
       exists x; split => //. right.
       exists x0. now split.
-    * pose proof (abstract_env_ext_exists X) as [[Σ wfΣ]].
+    * try clear Heqcall; pose proof (abstract_env_ext_exists X) as [[Σ wfΣ]].
       move => / (_ _ wfΣ) [[T' [HT' er]]].
       pose proof (abstract_env_ext_wf _ wfΣ) as [wf].
       move/is_arityP: Heq => nisa.

safechecker/theories/PCUICSafeConversion.v

@@ -1223,7 +1223,7 @@ Section Conversion.
       apply decompose_stack_at_appstack_None in e; eauto.
       destruct nth_error ; [|now right].
       left. eexists; split; eauto; cbn. now inversion eq1.
-    - destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
+    - try clear Heqcall. destruct (abstract_env_ext_exists X) as [[Σ wfΣ]].
       match type of eq3 with
       | _ = reduce_stack ?a ?b ?c ?d ?e ?f ?g =>
         pose proof (reduce_stack_sound a b c Σ wfΣ d e f g) as [r];
@@ -5578,15 +5578,15 @@ Qed.
       split; [eauto with pcuic|].
       apply whnf_mkApps.
       eapply whne_const; eauto.
-    - zip fold in h.
+    - zip fold in h. try clear Heqcall.
       destruct (hΣ _ wfΣ).
       eapply welltyped_context in h; eauto.
       destruct h as (?&typ); auto.
       apply inversion_Const in typ as (?&?&?&?); auto.
       unshelve eapply declared_constant_to_gen in d; eauto.
       clear H. erewrite <- abstract_env_lookup_correct' in e; eauto.
       congruence.
-    - zip fold in h.
+    - zip fold in h. try clear Heqcall.
       destruct (hΣ _ wfΣ).
       eapply welltyped_context in h; eauto.
       destruct h as (?&typ); auto.