From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 vernac/classes.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index ea434dbc4f..27d8b7390d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -374,7 +374,7 @@ let context poly l =
   let univs =
     match ctx with
     | [] -> assert false
-    | [_] -> Evd.const_univ_entry ~poly sigma
+    | [_] -> Evd.univ_entry ~poly sigma
     | _::_::_ ->
       if Lib.sections_are_opened ()
       then
@@ -384,19 +384,19 @@ let context poly l =
         begin
           let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
-          if poly then Polymorphic_const_entry ([||], Univ.UContext.empty)
-          else Monomorphic_const_entry Univ.ContextSet.empty
+          if poly then Polymorphic_entry ([||], Univ.UContext.empty)
+          else Monomorphic_entry Univ.ContextSet.empty
         end
       else if poly then
         (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
-        Evd.const_univ_entry ~poly sigma
+        Evd.univ_entry ~poly sigma
       else
         (* Multiple monomorphic axioms: declare universes separately
            to avoid redeclaring them. *)
         begin
           let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
-          Monomorphic_const_entry Univ.ContextSet.empty
+          Monomorphic_entry Univ.ContextSet.empty
         end
   in
   let fn status (id, b, t) =
-- 
cgit v1.2.3