From 0d9a91113c4112eece0680e433f435fdfb39ea4b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Jul 2017 16:33:47 +0200
Subject: Getting rid of simple calls to AUContext.instance.

This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
---
 pretyping/evarconv.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b5d195873c..2acf6bfe67 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -353,9 +353,8 @@ let exact_ise_stack2 env evd f sk1 sk2 =
 let check_leq_inductives evd cumi u u' =
   let u = EConstr.EInstance.kind evd u in
   let u' = EConstr.EInstance.kind evd u' in
-  let length_ind_instance = 
-    Univ.Instance.length
-      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+  let length_ind_instance =
+    Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
   in
   let ind_sbcst =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((length_ind_instance = Univ.Instance.length u) &&
-- 
cgit v1.2.3


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 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'pretyping/evarconv.ml')

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
 
-- 
cgit v1.2.3