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/evarconv.ml     | 4 +---
 pretyping/reductionops.ml | 6 ++----
 2 files changed, 3 insertions(+), 7 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2acf6bfe67..87f29ba492 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -363,9 +363,7 @@ let check_leq_inductives evd cumi u u' =
   else
     begin
      let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = 
-       Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst)
-     in
+     let comp_cst =  Univ.AUContext.instantiate comp_subst ind_sbcst in
      Evd.add_constraints evd comp_cst
     end
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3acefa1342..21ed8e0a23 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