 Timestamp:
 Nov 6, 2012, 3:17:23 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FrontEndOps.ma
r2395 r2432 409 409 [ Vptr ptr1 ⇒ match v2 with 410 410 [ Vptr ptr2 ⇒ 411 if eq_block (pblock ptr1) (pblock ptr2) then412 if (valid_pointer m ptr1 ∨ end_pointer m ptr1) ∧413 (valid_pointer m ptr2 ∨ end_pointer mptr2)411 if valid_pointer m ptr1 ∧ valid_pointer m ptr2 412 then 413 if eq_block (pblock ptr1) (pblock ptr2) 414 414 then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2))) 415 else None ? 416 else 417 if valid_pointer m ptr1 ∧ 418 valid_pointer m ptr2 419 then ev_cmp_mismatch c 420 else None ? 415 else ev_cmp_mismatch c 416 else None ? 421 417  Vnull ⇒ ev_cmp_mismatch c 422 418  _ ⇒ None ? ] … … 509 505 whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?);  ] #E destruct // 510 506  #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ] 511 whd in ⊢ (??%? → ?); [ cases (andb ??) cases ( andb ??) cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //507 whd in ⊢ (??%? → ?); [ cases (andb ??) cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct // 512 508 ] qed. 513 509
Note: See TracChangeset
for help on using the changeset viewer.