diff options
| author | Matthieu Sozeau | 2015-09-23 16:14:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:10 +0200 |
| commit | 72c6588923dca52be7bc7d750d969ff1baa76c45 (patch) | |
| tree | a8b46ecadae6fcf29b6c3dd504e557dfea444f4e /plugins/cc/ccalgo.ml | |
| parent | 26628315688e07c43b9881872a737454e93fe4c9 (diff) | |
Univs: fix an evar leak in congruence
Diffstat (limited to 'plugins/cc/ccalgo.ml')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index d5d6bdf749..97ea5fdc59 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -129,14 +129,14 @@ type cinfo= ci_nhyps: int} (* # projectable args *) let family_eq f1 f2 = match f1, f2 with -| InProp, InProp -| InSet, InSet -| InType, InType -> true -| _ -> false + | Prop Pos, Prop Pos + | Prop Null, Prop Null + | Type _, Type _ -> true + | _ -> false type term= Symb of constr - | Product of sorts_family * sorts_family + | Product of sorts * sorts | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) @@ -161,7 +161,7 @@ let hash_sorts_family = function let rec hash_term = function | Symb c -> combine 1 (hash_constr c) - | Product (s1, s2) -> combine3 2 (hash_sorts_family s1) (hash_sorts_family s2) + | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j @@ -425,8 +425,8 @@ let _B_ = Name (Id.of_string "A") let _body_ = mkProd(Anonymous,mkRel 2,mkRel 2) let cc_product s1 s2 = - mkLambda(_A_,mkSort(Universes.new_sort_in_family s1), - mkLambda(_B_,mkSort(Universes.new_sort_in_family s2),_body_)) + mkLambda(_A_,mkSort(s1), + mkLambda(_B_,mkSort(s2),_body_)) let rec constr_of_term = function Symb s-> applist_projection s [] |