diff options
| author | Gaëtan Gilbert | 2018-10-10 14:20:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:52:53 +0200 |
| commit | 44ecd58e9ab5fb0f2c45e9eec76440f84995825c (patch) | |
| tree | 5ce39ab09db09194d5a28ee48cd4a7ee7643b4fc /kernel/vars.mli | |
| parent | e99b4c66cf38bb5b6ccb76b69ebd7e7a44ed295d (diff) | |
{Univops -> Vars}.universes_of_constr
It's basically an occur check so it makes sense to put it in vars
Diffstat (limited to 'kernel/vars.mli')
| -rw-r--r-- | kernel/vars.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli index fdddbdb342..7c928e2694 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -139,3 +139,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context (** Instance substitution for polymorphism. *) val subst_instance_constr : Instance.t -> constr -> constr val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context + +val universes_of_constr : constr -> Univ.LSet.t |