Changeset 1401 for src/Cminor


Ignore:
Timestamp:
Oct 18, 2011, 12:39:11 PM (9 years ago)
Author:
ricciott
Message:

Changes concerning the new behavior of destruct.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1369 r1401  
    2424definition stmt_inv : stmt → Prop ≝
    2525  stmt_P (λs. stmt_vars (λ_.False) s ∧ stmt_labels (λ_.False) s).
     26 
     27discriminator option.
     28discriminator Sig.
    2629
    2730(* Produces a few extra skips - hopefully the compiler will optimise these
     
    3841].
    3942% //
    40 cases init in p; [ 8: #a #b ] #c #p normalize in p; destruct; /2/
     43cases init in p; [ 8: #a #b ] #c #p normalize in p;
     44destruct;/2/
    4145qed.
    4246
Note: See TracChangeset for help on using the changeset viewer.