Changeset 798 for src/Clight/CexecEquiv.ma
- Timestamp:
- May 13, 2011, 1:10:23 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/CexecEquiv.ma
r797 r798 367 367 | #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim 368 368 [ #r ] #F #EXEC whd in EXEC:(??%?); destruct 369 | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?) destruct @refl369 | #msg1 #msg2 #EXEC #E whd in EXEC:(??%?); destruct @refl 370 370 ] 371 371 | #o #k #i #e #H #EXEC #E destruct
Note: See TracChangeset
for help on using the changeset viewer.