Changeset 1401 for src/Clight


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/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) ≝
Note: See TracChangeset for help on using the changeset viewer.