Changeset 1947
- Timestamp:
- May 15, 2012, 12:30:13 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r1946 r1947 2206 2206 whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP 2207 2207 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/*) 2209 2214 |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?) 2210 2215 @Some_Some_elim #MAP cases (pol ?) normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.