diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-23 16:14:28 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
| commit | 72c6588923dca52be7bc7d750d969ff1baa76c45 (patch) | |
| tree | a8b46ecadae6fcf29b6c3dd504e557dfea444f4e /plugins/cc | |
| parent | 26628315688e07c43b9881872a737454e93fe4c9 (diff) | |
Univs: fix an evar leak in congruence
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 16 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.mli | 2 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 2 |
3 files changed, 10 insertions, 10 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index d5d6bdf74..97ea5fdc5 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 [] diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index c72843d55..0dcf3a870 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -30,7 +30,7 @@ type cinfo = 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 *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 9c3a0f729..6439f58d2 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -46,7 +46,7 @@ let whd_delta env= (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = family_of_sort (sort_of env (ref sigma) c) +let sf_of env sigma c = sort_of env (ref sigma) c let rec decompose_term env sigma t= match kind_of_term (whd env t) with |