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.
---
 checker/reduction.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'checker/reduction.ml')

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 93b8b907ca..0b605820d7 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -157,11 +157,11 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
   else raise NotConvertible
 
 let convert_inductive_instances cv_pb cumi u u' univs =
-  let ind_instance =
-      Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in
+  let len_instance =
+      Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
   let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+  if not ((len_instance = Univ.Instance.length u) &&
+          (len_instance = Univ.Instance.length u')) then
     anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
-- 
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.
---
 checker/reduction.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'checker/reduction.ml')

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 0b605820d7..6d8783d7e5 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -166,16 +166,14 @@ let convert_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
-- 
cgit v1.2.3