From 6390887ce1fd32c2180f373f1e701d9488c341f9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 5 Sep 2014 20:31:34 +0200 Subject: Remove unused substitution functions in checker. --- checker/univ.mli | 7 ------- 1 file changed, 7 deletions(-) (limited to 'checker/univ.mli') diff --git a/checker/univ.mli b/checker/univ.mli index 27f4c9a6e..89dd64486 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -197,19 +197,12 @@ val is_empty_level_subst : universe_level_subst -> bool val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level val subst_univs_level_universe : universe_level_subst -> universe -> universe -(** Make a universe level substitution: the instances must match. *) -val make_universe_subst : Instance.t -> universe_context -> universe_level_subst -(** Get the instantiated graph. *) -val instantiate_univ_context : universe_level_subst -> universe_context -> constraints - (** Level to universe substitutions. *) val is_empty_subst : universe_subst -> bool val make_subst : universe_subst -> universe_subst_fn val subst_univs_universe : universe_subst_fn -> universe -> universe -val subst_univs_constraints : universe_subst_fn -> constraints -> constraints - (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance -- cgit v1.2.3