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/univops.mli | |
| parent | 0b8c1aa84dc7200b055d45cf528a83163dfd21f8 (diff) | |
| parent | 40114382c04aafa1c8e1c156ca24a5ad1aa4b9fb (diff) | |
Merge PR #7906: universes_of_constr don't include universes of monomorphic constants
Diffstat (limited to 'engine/univops.mli')
| -rw-r--r-- | engine/univops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
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 |