Changeset 1947

Timestamp:

May 15, 2012, 12:30:13 AM (9 years ago)

Author:

sacerdot

Message:

Failure of automation/demod investigated a little bit.

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -2206 +2206 @@
    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
    whd in match (execute_1_pseudo_instruction0 ?????);
-   %{0} @split_eq_status CSC:STOP HERE //
+   %{0} @split_eq_status
+   CSC: STOP HERE, was // but requires -H0 -H3 because of \fst and \pi1
+   ⇒ CHANGE TO AVOID \fst and \pi1! (*
+   try (<H3 -H0 -H3 //)
+   [ <add_zero in H3; #H3 >H3 -H0 -H3 //
+   | -H0 -H3 /demod/*)
   |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
    @Some_Some_elim #MAP cases (pol ?) normalize nodelta