More naming work

MetaCoq · Apr 5, 2023 · 01505c5 · 01505c5
1 parent beab18b
commit 01505c5
Showing 1 changed file with 11 additions and 6 deletions.
diff --git a/erasure/theories/EWcbvEvalNamed.v b/erasure/theories/EWcbvEvalNamed.v
@@ -1340,6 +1340,7 @@ Proof.
     let X0 := match goal with H : All _ _ -> _ -> _ |- _ => H end in
     eapply X0. eapply wf_add_multiple; eauto.
     len. eapply All2_length in f4. lia.
+    let H := match goal with H : All (fun x => is_true (_ && _ && _)) _ |- _ => H end in
     eapply All_nth_error in H. 2: eauto. rtoProp.
     solve_all.
     rewrite map_fst_add_multiple. len.
@@ -1349,15 +1350,18 @@ Proof.
                  | nNamed na => [na]
                  end) br.1) as -> by eauto.
     clear - f4. induction f4; cbn; f_equal; destruct r, x; cbn; congruence.
-  - do 2 forward X; eauto. invs X.
+  - let X := match goal with H : All _ _ -> _ -> wf (vRecClos _ _ _) |- _ => H end in
+    do 2 forward X; eauto; invs X.
+    let X0 := match goal with H : All _ (add _ _ _) -> _ -> wf _ |- _ => H end in
     eapply X0.
     + econstructor; cbn; eauto.
       eapply wf_add_multiple; eauto.
       now rewrite map_length fix_env_length.
       eapply wf_fix_env; eauto.
-    + eapply All_nth_error in X2; eauto. cbn in X2. rtoProp.
-      rewrite map_fst_add_multiple. now rewrite map_length fix_env_length.
-      eauto.
+    + let X2 := multimatch goal with H : All _ _ |- _ => H end in
+      eapply All_nth_error in X2; eauto; cbn in X2; rtoProp;
+      rewrite map_fst_add_multiple; first [ now rewrite map_length fix_env_length
+      | eauto ].
   - assert (map fst (MCList.map2 (λ (n : ident) (d0 : def term), (n, EAst.dbody d0)) nms mfix) = nms) as EE. {
     clear - f6. induction f6; cbn; f_equal; eauto. }
     econstructor.
@@ -1404,9 +1408,10 @@ Proof.
       destruct r as [[? []]].
       destruct x; cbn in *; subst; eauto.
    + eauto.
-  - eapply X; eauto. eapply declared_constant_Forall in isdecl.
+  - let X := match goal with H : All _ _ -> _ -> wf _ |- _ => H end in
+    eapply X; eauto. eapply declared_constant_Forall in isdecl.
     2: eapply Forall_impl. 2: eauto.
-    2: { cbn. intros [] ?. cbn in *.  exact H. }
+    2: { cbn. intros [] ?. cbn in *. let H := match goal with H : match _ with ConstantDecl _ => _ | _ => _ end |- _ => H end in exact H. }
     cbn in *. destruct decl; cbn in *.
     subst. eauto.
   - solve_all. econstructor.