Ignore:
Timestamp:
Mar 23, 2011, 2:28:55 PM (9 years ago)
Author:
campbell
Message:

Use a more normalize-friendly definition of clight_exec to make the destruct
tactic usable again, and recomplete the equivalence proof.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r700 r708  
    455455| #f #l #s #k #env #m @refl
    456456] qed.
     457
     458lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r.
     459#s0 #r0 * #r #m @refl qed.
     460 
Note: See TracChangeset for help on using the changeset viewer.