diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 18 | ||||
| -rw-r--r-- | engine/eConstr.mli | 4 |
2 files changed, 22 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index afdceae061..ea098902a2 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -645,6 +645,24 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None +let universes_of_constr sigma c = + let open Univ in + let rec aux s c = + match kind sigma c with + | Const (_, u) | Ind (_, u) | Construct (_, u) -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Sort u -> + let sort = ESorts.kind sigma u in + if Sorts.is_small sort then s + else + let u = Sorts.univ_of_sort sort in + LSet.fold LSet.add (Universe.levels u) s + | Evar (k, args) -> + let concl = Evd.evar_concl (Evd.find sigma k) in + fold sigma aux (aux s (of_constr concl)) c + | _ -> fold sigma aux s c + in aux LSet.empty c + open Context open Environ diff --git a/engine/eConstr.mli b/engine/eConstr.mli index e9ef302cf6..3e6a13f709 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -201,6 +201,10 @@ val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit 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 : Evd.evar_map -> t -> Univ.LSet.t + (** {6 Substitutions} *) module Vars : |