Changeset 1353 for src/common


Ignore:
Timestamp:
Oct 11, 2011, 12:45:59 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1350 r1353  
    199199
    200200lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
    201 * *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.
     201* *; try *; try *; try *; try *; try (%1 @refl) %2 @nmk #H cases daemon (*Wilmer: XXX*) qed.
    202202
    203203lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
     
    288288
    289289definition prog_funct_names ≝ λF,V. λp: program F V.
    290   map \fst (prog_funct … p).
     290  map ?? \fst (prog_funct … p).
    291291
    292292definition prog_var_names ≝ λF,V. λp: program F V.
    293   map (λx. \fst (\fst x)) (prog_vars … p).
     293  map ?? (λx. \fst (\fst x)) (prog_vars … p).
    294294
    295295(* * * Generic transformations over programs *)
Note: See TracChangeset for help on using the changeset viewer.