Changeset 1401


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

Changes concerning the new behavior of destruct.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/TypeComparison.ma

    r1352 r1401  
    8787        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
    8888        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
    89 ]. (*Wilmer:XXXX try destruct //*) cases daemon qed.
     89]. try destruct; //
     90qed.
    9091
    9192definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
  • 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
  • src/common/AST.ma

    r1368 r1401  
    199199
    200200lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    201 * #H [#H2] * #H' (try #H2') try (%1 @refl) [2,3,4,6,7,8: %2 @nmk #abs destruct]
    202 cases H cases H' try (%1 @refl) [1,5,9: cases H2 cases H2' try (%1 @refl)]
    203 %2 @nmk #abs -H H'; destruct (abs) (*Wilmer: still slow destructs, why?*)
     201* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct
    204202qed.
    205203
Note: See TracChangeset for help on using the changeset viewer.