diff options
Diffstat (limited to 'kernel/vars.mli')
| -rw-r--r-- | kernel/vars.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli index 7c928e2694..f2c32b3625 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -140,4 +140,7 @@ val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context val subst_instance_constr : Instance.t -> constr -> constr val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context +val univ_instantiate_constr : Instance.t -> constr univ_abstracted -> constr +(** Ignores the constraints carried by [univ_abstracted]. *) + val universes_of_constr : constr -> Univ.LSet.t |