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.
---
 kernel/cbytegen.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/cbytegen.mli')

diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index b1b55aef48..6a9550342c 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -20,7 +20,7 @@ val compile : fail_on_error:bool ->
 (** init, fun, fv *)
 
 val compile_constant_body : fail_on_error:bool ->
-  env -> constant_universes -> Constr.t Mod_subst.substituted constant_def ->
+  env -> universes -> Constr.t Mod_subst.substituted constant_def ->
   body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
-- 
cgit v1.2.3