Ignore:
Timestamp:
Feb 21, 2012, 11:58:12 AM (8 years ago)
Author:
campbell
Message:

Add a distinguished final state to the front-end languages to match up
with the structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r1672 r1713  
    456456    #H whd in ⊢ (??%?); >H @refl
    457457| #f #l #s #k #env #m @refl
     458| #r #m //
    458459] qed.
    459460
    460461lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r.
    461 #s0 #r0 * #r #m @refl qed.
     462#s0 #r0 * #r @refl qed.
    462463 
Note: See TracChangeset for help on using the changeset viewer.