Changeset 2176 for src/Clight/labelSimulation.ma
- Timestamp:
- Jul 12, 2012, 1:28:28 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/labelSimulation.ma
r2145 r2176 103 103 whd in ⊢ (?(??%?)?); 104 104 cases ty' in EX1rem ⊢ %; 105 [ 4: #r #ty' whd in ⊢ (??%? → ?(??%?)?); cases (pointer_compat_dec b1 r) 106 #pc normalize #E destruct /2/ 105 [ 4: #ty' normalize #E destruct /2/ 107 106 | *: normalize #A try #B try #C try #D destruct 108 107 ] … … 672 671 % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E @refl 673 672 | // ] | /3/ ] 674 | *: #A [ 1, 3,5,6,7,8: #B | 4: #B #C] #E >E in EX; #EX whd in EX:(??%%); destruct673 | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct 675 674 ] 676 675 | #u #s0 #k0 #k0' #K #_ #E1 #E2 #E3 destruct %{tr} … … 720 719 %{E0} % [2: % [ % [ @plus_one whd in ⊢ (??%?); >label_function_return >E in ⊢ (??%?); 721 720 @refl | // ] | /4/ ] | skip ] 722 | *: #A [ 1, 3,5,6,7,8: #B | 4: #B #C] #E >E in EX; #EX whd in EX:(??%%); destruct721 | *: #A [ 1,4,5,6,7: #B ] #E >E in EX; #EX whd in EX:(??%%); destruct 723 722 ] 724 723 | #ls #u #k0 #k0' #K #_ #E1 #E2 #E3 destruct whd in EX:(??%?); destruct
Note: See TracChangeset
for help on using the changeset viewer.