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.
---
 API/API.mli | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 5c78606715..ad5d5490b8 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1417,7 +1417,7 @@ sig
     | TemplateArity of 'b
 
   type constant_universes =
-    | Monomorphic_const of Univ.UContext.t
+    | Monomorphic_const of Univ.ContextSet.t
     | Polymorphic_const of Univ.AUContext.t
 
   type projection_body = {
@@ -1484,7 +1484,7 @@ sig
                        | MEwith of module_alg_expr * with_declaration
 
   type abstract_inductive_universes =
-  | Monomorphic_ind of Univ.UContext.t
+  | Monomorphic_ind of Univ.ContextSet.t
   | Polymorphic_ind of Univ.AUContext.t
   | Cumulative_ind of Univ.ACumulativityInfo.t
 
@@ -1551,7 +1551,7 @@ sig
     | LocalAssumEntry of constr
 
   type inductive_universes =
-    | Monomorphic_ind_entry of Univ.UContext.t
+    | Monomorphic_ind_entry of Univ.ContextSet.t
     | Polymorphic_ind_entry of Univ.UContext.t
     | Cumulative_ind_entry of Univ.CumulativityInfo.t
 
@@ -1580,8 +1580,9 @@ sig
   type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a
   type 'a const_entry_body = 'a proof_output Future.computation
   type constant_universes_entry =
-    | Monomorphic_const_entry of Univ.UContext.t
+    | Monomorphic_const_entry of Univ.ContextSet.t
     | Polymorphic_const_entry of Univ.UContext.t
+  type 'a in_constant_universes_entry = 'a * constant_universes_entry
   type 'a definition_entry =
                                { const_entry_body   : 'a const_entry_body;
                                  (* List of section variables *)
@@ -1592,7 +1593,7 @@ sig
                                  const_entry_universes   : constant_universes_entry;
                                  const_entry_opaque      : bool;
                                  const_entry_inline_code : bool }
-  type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline
+  type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline
 
   type projection_entry = {
     proj_entry_ind : MutInd.t;
-- 
cgit v1.2.3