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. --- pretyping/reductionops.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'pretyping/reductionops.ml') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3acefa134..21ed8e0a2 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1372,15 +1372,13 @@ let sigma_check_inductive_instances cv_pb uinfind u u' sigma = else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbctx) + Univ.AUContext.instantiate comp_subst ind_sbctx in let comp_cst = match cv_pb with Reduction.CONV -> let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = - Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx) - in + let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in Univ.Constraint.union comp_cst comp_cst' | Reduction.CUMUL -> comp_cst in -- cgit v1.2.3