diff options
Diffstat (limited to 'kernel/vars.mli')
| -rw-r--r-- | kernel/vars.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli index ef3381ab5..9d5d16d0c 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -68,3 +68,17 @@ val subst_vars : Id.t list -> constr -> constr (** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t] if two names are identical, the one of least indice is kept *) val substn_vars : int -> Id.t list -> constr -> constr + +(** {3 Substitution of universes} *) + +open Univ + +val subst_univs_fn_constr : universe_subst_fn -> constr -> constr +val subst_univs_fn_puniverses : universe_level_subst_fn -> + 'a puniverses -> 'a puniverses + +val subst_univs_constr : universe_subst -> constr -> constr +val subst_univs_puniverses : universe_level_subst -> 'a puniverses -> 'a puniverses +val subst_univs_level_constr : universe_level_subst -> constr -> constr + +val subst_univs_context : Univ.universe_subst -> rel_context -> rel_context |