From 4457e6d75affd20c1c13c0d798c490129525bcb5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Jul 2017 13:38:22 +0200
Subject: More precise type for universe entries.

We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
---
 API/API.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index bb24d5768f..4d9904b5f5 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1345,6 +1345,9 @@ sig
   type inline = int option
   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.universe_context
+    | Polymorphic_const_entry of Univ.universe_context
   type 'a definition_entry =
                                { const_entry_body   : 'a const_entry_body;
                                  (* List of section variables *)
@@ -1352,8 +1355,7 @@ sig
                                  (* State id on which the completion of type checking is reported *)
                                  const_entry_feedback    : Stateid.t option;
                                  const_entry_type        : Constr.types option;
-                                 const_entry_polymorphic : bool;
-                                 const_entry_universes   : Univ.UContext.t;
+                                 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
-- 
cgit v1.2.3