From b8a7222e670f69e024d50394afd88204e15d1b29 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 10 Jul 2017 18:05:23 +0200 Subject: Less footguns in universe handling: remove subst_instance_context. This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone. --- checker/univ.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'checker/univ.mli') diff --git a/checker/univ.mli b/checker/univ.mli index faa682cbf..75c76cd12 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -211,6 +211,8 @@ sig val instance : t -> Instance.t val size : t -> int + val instantiate : Instance.t -> t -> Constraint.t + end type abstract_universe_context = AUContext.t @@ -277,7 +279,6 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe (** Substitution of instances *) val subst_instance_instance : universe_instance -> universe_instance -> universe_instance val subst_instance_universe : universe_instance -> universe -> universe -val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context (* val make_instance_subst : universe_instance -> universe_level_subst *) (* val make_inverse_instance_subst : universe_instance -> universe_level_subst *) -- cgit v1.2.3