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.
---
 tactics/ind_tables.ml | 8 ++++++--
 tactics/tactics.ml    | 8 +++++---
 2 files changed, 11 insertions(+), 5 deletions(-)

(limited to 'tactics')

diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 0407c1e36a..7f087ea01a 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,14 +123,18 @@ 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 =
+    if p then Polymorphic_const_entry univs
+    else Monomorphic_const_entry univs
+  in
   let entry = {
     const_entry_body =
       Future.from_val ((c,Univ.ContextSet.empty),
                        Safe_typing.empty_private_constants);
     const_entry_secctx = None;
     const_entry_type = None;
-    const_entry_polymorphic = p;
-    const_entry_universes = Evd.evar_context_universe_context ctx;
+    const_entry_universes = univs;
     const_entry_opaque = false;
     const_entry_inline_code = false;
     const_entry_feedback = None;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a95ad177d..cb905e749a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5004,8 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
   in
   let cst = Impargs.with_implicit_protection cst () in
   let lem =
-    if const.Entries.const_entry_polymorphic then
-      let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in
+    match const.Entries.const_entry_universes with
+    | Entries.Polymorphic_const_entry uctx ->
+      let uctx = Univ.ContextSet.of_context uctx in
       (** Hack: the kernel may generate definitions whose universe variables are
           not the same as requested in the entry because of constraints delayed
           in the body, even in polymorphic mode. We mimick what it does for now
@@ -5014,7 +5015,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
       let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in
       let u = Univ.UContext.instance uctx in
       mkConstU (cst, EInstance.make u)
-    else mkConst cst
+    | Entries.Monomorphic_const_entry _ ->
+      mkConst cst
   in
   let evd = Evd.set_universe_context evd ectx in
   let open Safe_typing in
-- 
cgit v1.2.3