Ignore:
Timestamp:
Jun 3, 2011, 5:35:32 PM (9 years ago)
Author:
campbell
Message:

Fix up fragile proofs for current version of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/TypeComparison.ma

    r880 r882  
    1313definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).
    1414#n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E
    15 [ %1 | %2 ] @(eqb_elim … E) // #_ #H destruct qed.
     15[ %1 | %2 ] lapply E @eqb_elim // #_ #H destruct qed.
    1616
    1717let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
Note: See TracChangeset for help on using the changeset viewer.