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.
---
 interp/declare.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/declare.mli')

diff --git a/interp/declare.mli b/interp/declare.mli
index 669657af6f..6f53d6872b 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -43,7 +43,7 @@ type internal_flag =
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?univs:Entries.constant_universes_entry ->
+  ?univs:Entries.universes_entry ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 (** [declare_constant id cd] declares a global declaration
@@ -58,7 +58,7 @@ val declare_constant :
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> Id.t -> ?types:constr ->
-  constr Entries.in_constant_universes_entry -> Constant.t
+  constr Entries.in_universes_entry -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
-- 
cgit v1.2.3