From bad3f3b784d3de8851615b8f4b7afba734232d8e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Dec 2017 17:33:04 +0100 Subject: Moving some universe substitution code out of the kernel. This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper. --- kernel/vars.mli | 6 ------ 1 file changed, 6 deletions(-) (limited to 'kernel/vars.mli') diff --git a/kernel/vars.mli b/kernel/vars.mli index 964de4e95..b74d25260 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -129,12 +129,6 @@ val subst_var : Id.t -> constr -> constr 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 - (** Level substitutions for polymorphism. *) val subst_univs_level_constr : universe_level_subst -> constr -> constr -- cgit v1.2.3