Changeset 1947


Ignore:
Timestamp:
May 15, 2012, 12:30:13 AM (7 years ago)
Author:
sacerdot
Message:

Failure of automation/demod investigated a little bit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r1946 r1947  
    22062206   whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
    22072207   whd in match (execute_1_pseudo_instruction0 ?????);
    2208    %{0} @split_eq_status CSC:STOP HERE //
     2208   %{0} @split_eq_status
     2209   CSC: STOP HERE, was // but requires -H0 -H3 because of \fst and \pi1
     2210   ⇒ CHANGE TO AVOID \fst and \pi1! (*
     2211   try (<H3 -H0 -H3 //)
     2212   [ <add_zero in H3; #H3 >H3 -H0 -H3 //
     2213   | -H0 -H3 /demod/*)
    22092214  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
    22102215   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.