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.
---
 engine/evd.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'engine/evd.ml')

diff --git a/engine/evd.ml b/engine/evd.ml
index eee2cb700c..f0433d3387 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -852,8 +852,9 @@ let universe_context_set d = UState.context_set d.universes
 
 let to_universe_context evd = UState.context evd.universes
 
-let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes
-let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes
+let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
+
+let const_univ_entry = univ_entry
 
 let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
 
-- 
cgit v1.2.3