Fix PASS PROOF

snu-sf · Jul 9, 2019 · 9c556da · 9c556da
1 parent 8fdb8d9
commit 9c556da
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/backend/CSEproofC.v b/backend/CSEproofC.v
@@ -72,7 +72,7 @@ Proof.
     exploit make_match_genvs; eauto. { apply SIMSKENV. } intro SIMGE.
     exploit (Genv.find_funct_match_genv SIMGE); eauto. i; des. ss. unfold bind in *. folder. des_ifs.
     inv TYP. unfold transf_function in *. des_ifs.
-    esplits; eauto. econs; eauto.
+    esplits; eauto. econs; swap 1 2; eauto; ss.
     + econs; eauto.
       erewrite <- lessdef_list_length; eauto.
     + erewrite <- lessdef_list_length; eauto.

diff --git a/backend/ConstpropproofC.v b/backend/ConstpropproofC.v
@@ -64,7 +64,7 @@ Proof.
     des. inv SAFESRC. inv SIMARGS; ss. inv FPTR; ss.
     exploit make_match_genvs; eauto. { apply SIMSKENV. } intro SIMGE.
     exploit (Genv.find_funct_match_genv SIMGE); eauto. i; des. ss. des_ifs.
-    inv TYP. esplits; eauto. econs; eauto.
+    inv TYP. esplits; eauto. econs; swap 1 2; eauto.
     + econs; eauto with congruence.
       erewrite <- lessdef_list_length; eauto.
     + erewrite <- lessdef_list_length; eauto.

diff --git a/backend/DeadcodeproofC.v b/backend/DeadcodeproofC.v
@@ -72,7 +72,7 @@ Proof.
     exploit make_match_genvs; eauto. { apply SIMSKENV. } intro SIMGE.
     exploit (Genv.find_funct_match_genv SIMGE); eauto. i; des. ss. unfold bind in *. folder. des_ifs.
     inv TYP. unfold transf_function in *. des_ifs.
-    esplits; eauto. econs; eauto.
+    esplits; eauto. econs; swap 1 2; eauto.
     + econs; eauto. erewrite <- lessdef_list_length; eauto.
     + erewrite <- lessdef_list_length; eauto.
   - (* call wf *)

diff --git a/backend/InliningproofC.v b/backend/InliningproofC.v
@@ -88,7 +88,7 @@ Proof.
     exploit (Genv.find_funct_match_genv SIMGE); eauto. i; des. ss. clarify. folder.
     hexploit (@fsim_external_inject_eq); try apply FINDF; eauto. clear FPTR. intro FPTR.
     unfold Errors.bind in *. unfold transf_function in *. des_ifs. inv TYP.
-    esplits; eauto. econs; eauto.
+    esplits; eauto. econs; swap 1 2; eauto.
     + econs; eauto. erewrite <- inject_list_length; eauto.
     + erewrite <- inject_list_length; eauto.
   - (* call wf *)