From d437078a4ca82f7ca6d19be5ee9452359724f9a0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 15:46:30 +0200
Subject: Use Maps and ids for universe binders

Before sometimes there were lists and strings.
---
 engine/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 60bd6de2ae..ca1196b948 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -802,7 +802,7 @@ let make_evar_universe_context e l =
   | Some us ->
       List.fold_left
         (fun uctx (loc,id) ->
-        fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx))
+        fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx))
         uctx us
 
 (****************************************)
-- 
cgit v1.2.3


From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 21:01:57 +0200
Subject: Separate checking univ_decls and obtaining universe binder names.

---
 engine/evd.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index ca1196b948..67ae73ceb2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -936,6 +936,8 @@ let universe_of_name evd s = UState.universe_of_name evd.universes s
 let add_universe_name evd s l =
   { evd with universes = UState.add_universe_name evd.universes s l }
 
+let universe_binders evd = UState.universe_binders evd.universes
+
 let universes evd = UState.ugraph evd.universes
 
 let update_sigma_env evd env =
-- 
cgit v1.2.3


From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 22:21:46 +0200
Subject: Stop exposing UState.universe_context and its Evd wrapper.

We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
---
 engine/evd.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 67ae73ceb2..eb0f2e3e74 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -756,8 +756,7 @@ let evar_universe_context d = d.universes
 
 let universe_context_set d = UState.context_set d.universes
 
-let universe_context ~names ~extensible evd =
-  UState.universe_context ~names ~extensible evd.universes
+let to_universe_context evd = UState.context evd.universes
 
 let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
 
-- 
cgit v1.2.3


From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Sep 2017 17:22:24 +0200
Subject: Use Entries.constant_universes_entry more.

This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
---
 engine/evd.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index eb0f2e3e74..9ea2cc00f5 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -758,7 +758,10 @@ let universe_context_set d = UState.context_set d.universes
 
 let to_universe_context evd = UState.context evd.universes
 
-let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
+let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes
+let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes
+
+let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
 
 let restrict_universe_context evd vars =
   { evd with universes = UState.restrict evd.universes vars }
-- 
cgit v1.2.3


From d071eac98b7812ac5c03004b438022900885d874 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 21 Sep 2017 11:14:11 +0200
Subject: Forbid repeated names in universe binders.

---
 engine/evd.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index 9ea2cc00f5..0f17e0dc6d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -935,9 +935,6 @@ let nf_constraints evd =
 
 let universe_of_name evd s = UState.universe_of_name evd.universes s
 
-let add_universe_name evd s l =
-  { evd with universes = UState.add_universe_name evd.universes s l }
-
 let universe_binders evd = UState.universe_binders evd.universes
 
 let universes evd = UState.ugraph evd.universes
-- 
cgit v1.2.3