diff options
| author | Maxime Dénès | 2018-12-12 10:13:58 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 10:13:58 +0100 |
| commit | 84a950c8e1fa06d0dd764e9a426edbd987a7989e (patch) | |
| tree | 824e99b1dbb0cac36e16b0b1ac871bc3492eb2f1 /kernel/vars.mli | |
| parent | d87c4c472478fbcb30de6efabc68473ee36849a1 (diff) | |
| parent | 4db7296d629f08c5a71905d8f6d29e2c4e4c0517 (diff) | |
Merge PR #8974: Fix mod_subst wrt universe polymorphism
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 |