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.

---
 tactics/leminv.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 62f3866de9..4d1b271d6b 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -235,9 +235,9 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     p, Evd.universe_context ~names:[] ~extensible:true sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
-  let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
+  let invProof, univs = inversion_scheme env sigma t sort dep inv_op in
   let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
-			       ~univs:(snd ctx) invProof in
+                               ~univs invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
-- 
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).
---
 tactics/ind_tables.ml | 2 +-
 tactics/leminv.ml     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e7fa555c2b..92c326b1e7 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,7 +123,7 @@ let define internal id c p univs =
   let ctx = Evd.normalize_evar_universe_context univs in
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
-  let univs = Evd.evar_context_universe_context ctx in
+  let univs = UState.context ctx in
   let univs =
     if p then Polymorphic_const_entry univs
     else Monomorphic_const_entry univs
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 4d1b271d6b..1ee873e0ff 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,7 +232,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
   let invProof = EConstr.Unsafe.to_constr invProof in
   let p = Evarutil.nf_evars_universes sigma invProof in
-    p, Evd.universe_context ~names:[] ~extensible:true sigma
+    p, Evd.to_universe_context sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof, univs = inversion_scheme env sigma t sort dep inv_op in
-- 
cgit v1.2.3


From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Sep 2017 14:50:07 +0200
Subject: When declaring constants/inductives use ContextSet if monomorphic.

Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.

There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
---
 tactics/ind_tables.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 92c326b1e7..e1bf32f3ce 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,10 +123,9 @@ let define internal id c p univs =
   let ctx = Evd.normalize_evar_universe_context univs in
   let c = Vars.subst_univs_fn_constr 
     (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
-  let univs = UState.context ctx in
   let univs =
-    if p then Polymorphic_const_entry univs
-    else Monomorphic_const_entry univs
+    if p then Polymorphic_const_entry (UState.context ctx)
+    else Monomorphic_const_entry (UState.context_set ctx)
   in
   let entry = {
     const_entry_body =
-- 
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.
---
 tactics/leminv.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1ee873e0ff..1ae3577edb 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,12 +232,15 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
   let invProof = EConstr.Unsafe.to_constr invProof in
   let p = Evarutil.nf_evars_universes sigma invProof in
-    p, Evd.to_universe_context sigma
+    p, sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
-  let invProof, univs = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
-                               ~univs invProof in
+  let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
+  let univs =
+    let poly = Flags.use_polymorphic_flag () in
+    Evd.const_univ_entry ~poly sigma
+  in
+  let entry = definition_entry ~univs invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
-- 
cgit v1.2.3