diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-26 15:56:28 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-26 15:56:28 +0200 |
commit | b98ae49d282f73343c1950e960f4b3bc7c28de70 (patch) | |
tree | 53114d948cc278ca0a98e0a19e0ca9282ee891cd /engine | |
parent | 0b8c1aa84dc7200b055d45cf528a83163dfd21f8 (diff) | |
parent | 40114382c04aafa1c8e1c156ca24a5ad1aa4b9fb (diff) |
Merge PR #7906: universes_of_constr don't include universes of monomorphic constants
Diffstat (limited to 'engine')
-rw-r--r-- | engine/eConstr.ml | 13 | ||||
-rw-r--r-- | engine/eConstr.mli | 2 | ||||
-rw-r--r-- | engine/univops.ml | 15 | ||||
-rw-r--r-- | engine/univops.mli | 4 |
4 files changed, 6 insertions, 28 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 6810626ad..005ef1635 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -592,25 +592,14 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' 0 (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None -let universes_of_constr env sigma c = +let universes_of_constr sigma c = let open Univ in - let open Declarations in let rec aux s c = match kind sigma c with | Const (c, u) -> - begin match (Environ.lookup_constant c env).const_universes with - | Polymorphic_const _ -> LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s - | Monomorphic_const (univs, _) -> - LSet.union s univs - end | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - begin match (Environ.lookup_mind mind env).mind_universes with - | Cumulative_ind _ | Polymorphic_ind _ -> LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s - | Monomorphic_ind (univs,_) -> - LSet.union s univs - end | Sort u -> let sort = ESorts.kind sigma u in if Sorts.is_small sort then s diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e9d3e782b..913825a9f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -232,7 +232,7 @@ val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a (** Gather the universes transitively used in the term, including in the type of evars appearing in it. *) -val universes_of_constr : Environ.env -> Evd.evar_map -> t -> Univ.LSet.t +val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t (** {6 Substitutions} *) diff --git a/engine/univops.ml b/engine/univops.ml index 3fd518490..7f9672f82 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -11,24 +11,13 @@ open Univ open Constr -let universes_of_constr env c = - let open Declarations in - let rec aux s c = +let universes_of_constr c = + let rec aux s c = match kind c with | Const (c, u) -> - begin match (Environ.lookup_constant c env).const_universes with - | Polymorphic_const _ -> LSet.fold LSet.add (Instance.levels u) s - | Monomorphic_const (univs, _) -> - LSet.union s univs - end | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - begin match (Environ.lookup_mind mind env).mind_universes with - | Cumulative_ind _ | Polymorphic_ind _ -> LSet.fold LSet.add (Instance.levels u) s - | Monomorphic_ind (univs,_) -> - LSet.union s univs - end | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in LSet.fold LSet.add (Universe.levels u) s diff --git a/engine/univops.mli b/engine/univops.mli index 0b37ab975..57a53597b 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -11,8 +11,8 @@ open Constr open Univ -(** The universes of monomorphic constants appear. *) -val universes_of_constr : Environ.env -> constr -> LSet.t +(** Return the set of all universes appearing in [constr]. *) +val universes_of_constr : constr -> LSet.t (** [restrict_universe_context (univs,csts) keep] restricts [univs] to the universes in [keep]. The constraints [csts] are adjusted so |