Changeset 1352 for src/Clight


Ignore:
Timestamp:
Oct 11, 2011, 12:45:16 PM (8 years ago)
Author:
sacerdot
Message:

This commit is made necessary by the last Matita change.
Inclusion is now order of magnitudes faster in some situations.
However, some explicit "include alias" are now required to
achieve the old semantics.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecEquiv.ma

    r1350 r1352  
    44
    55include "basics/jmeq.ma".
     6include alias "basics/logic.ma".
    67
    78(* A "single execution" - where all of the input values are made explicit. *)
  • src/Clight/TypeComparison.ma

    r1350 r1352  
    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 ]. try destruct // (*Wilmer:XXXX*) cases daemon qed.
     89]. (*Wilmer:XXXX try destruct //*) cases daemon qed.
    9090
    9191definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
Note: See TracChangeset for help on using the changeset viewer.