Changeset 2588 for src/Clight/CexecComplete.ma
 Timestamp:
 Jan 23, 2013, 2:38:06 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecComplete.ma
r2468 r2588 194 194 >(yields_eq ??? H5) 195 195 @refl 196  #e1 #e2 #ty #v1 #tr # H1 #H2#H3 whd in ⊢ (??%?);196  #e1 #e2 #ty #v1 #tr #vres #H1 #H2 #Hcast #H3 whd in ⊢ (??%?); 197 197 >(yields_eq ??? H3) whd in ⊢ (??%?); 198 198 >(yields_eq ??? (bool_of_true ?? H2)) 199 @refl200  #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 # H1 #H2 #H3 #H4#H5 #H6 whd in ⊢ (??%?);199 >Hcast @refl 200  #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #vres #H1 #H2 #H3 #H4 #Hcast #H5 #H6 whd in ⊢ (??%?); 201 201 >(yields_eq ??? H5) whd in ⊢ (??%?); 202 202 >(yields_eq ??? (bool_of_false ?? H2)) … … 204 204 elim (bool_of_val_3_complete … H4); #b *; #evb #Hb 205 205 >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb 206 @refl 207  #e1 #e2 #ty #v1 #tr #H1 #H2 #H3 whd in ⊢ (??%?); 206 >Hcast 207 @refl 208  #e1 #e2 #ty #v1 #tr #vres #H1 #H2 #Hcast #H3 whd in ⊢ (??%?); 208 209 >(yields_eq ??? H3) whd in ⊢ (??%?); 209 210 >(yields_eq ??? (bool_of_false ?? H2)) 210 @refl 211  #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #H1 #H2 #H3 #H4 #H5 #H6 whd in ⊢ (??%?); 211 >Hcast 212 @refl 213  #e1 #e2 #ty #v1 #v2 #v #tr1 #tr2 #vres #H1 #H2 #H3 #H4 #Hcast #H5 #H6 whd in ⊢ (??%?); 212 214 >(yields_eq ??? H5) whd in ⊢ (??%?); 213 215 >(yields_eq ??? (bool_of_true ?? H2)) … … 215 217 elim (bool_of_val_3_complete … H4); #b *; #evb #Hb 216 218 >(yields_eq ??? Hb) whd in ⊢ (??%?); <evb 219 >Hcast normalize 217 220 @refl 218 221  #e #ty #ty' #v1 #v #tr #H1 #H2 #H3 whd in ⊢ (??%?);
Note: See TracChangeset
for help on using the changeset viewer.