Changeset 2184
- Timestamp:
- Jul 13, 2012, 7:59:41 PM (9 years ago)
- Location:
- src
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/SimplifyCasts.ma
r2176 r2184 3036 3036 whd in match (exec_step ??) in ⊢ (% → %); 3037 3037 #Habsurd destruct (Habsurd) 3038 ] 3038 ] qed. -
src/RTLabs/Traces.ma
r2044 r2184 799 799 >Estmt #LP whd in ⊢ (??%? → ?); 800 800 (* replace with lemma on successors? *) 801 @bind_res_value #a cases a [ | #sz #i | #f | #r| #ptr ] #Ea whd in ⊢ (??%? → ?);801 @bind_res_value #a cases a [ | #sz #i | #f | | #ptr ] #Ea whd in ⊢ (??%? → ?); 802 802 [ 2: (* later *) 803 803 | *: #E destruct … … 836 836 cases fd 837 837 [ #fn whd in ⊢ (??%? → % → ?); 838 @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)838 @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData) 839 839 #m' #b whd in ⊢ (??%? → ?); #E' destruct 840 840 * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3 … … 1497 1497 | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] // 1498 1498 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev 1499 cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | # r #E normalize in E; destruct | #p #E normalize in E; destruct ]1499 cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ] 1500 1500 whd in ⊢ (??%? → ?); 1501 1501 generalize in ⊢ (??(?%)? → ?); … … 1589 1589 | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl 1590 1590 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev 1591 cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | # r #E normalize in E; destruct | #p #E normalize in E; destruct ]1591 cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ] 1592 1592 whd in ⊢ (??%? → ?); 1593 1593 generalize in ⊢ (??(?%)? → ?);
Note: See TracChangeset
for help on using the changeset viewer.