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. --- kernel/reduction.ml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'kernel/reduction.ml') diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 423e0d934..2bf9f43a5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -689,16 +689,14 @@ let check_inductive_instances cv_pb cumi u u' univs = else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.UContext.constraints - (Univ.subst_instance_context comp_subst ind_subtypctx) + Univ.AUContext.instantiate comp_subst ind_subtypctx in let comp_cst = match cv_pb with CONV -> let comp_cst' = let comp_subst = (Univ.Instance.append u' u) in - Univ.UContext.constraints - (Univ.subst_instance_context comp_subst ind_subtypctx) + Univ.AUContext.instantiate comp_subst ind_subtypctx in Univ.Constraint.union comp_cst comp_cst' | CUMUL -> comp_cst @@ -775,16 +773,15 @@ let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) = else let comp_cst = let comp_subst = (Univ.Instance.append u u') in - Univ.UContext.constraints - (Univ.subst_instance_context comp_subst ind_subtypctx) + Univ.AUContext.instantiate comp_subst ind_subtypctx in let comp_cst = match cv_pb with CONV -> let comp_cst' = let comp_subst = (Univ.Instance.append u' u) in - Univ.UContext.constraints - (Univ.subst_instance_context comp_subst ind_subtypctx) in + Univ.AUContext.instantiate comp_subst ind_subtypctx + in Univ.Constraint.union comp_cst comp_cst' | CUMUL -> comp_cst in -- cgit v1.2.3