Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

1 files changed, 1 insertions, 1 deletions

diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 07c6f37fab..89b5c60ad5 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -20,7 +20,7 @@ type inline = bool
 type result = {
   cook_body : constr Mod_subst.substituted constant_def;
   cook_type : types;
-  cook_universes : constant_universes;
+  cook_universes : universes;
   cook_private_univs : Univ.ContextSet.t option;
   cook_inline : inline;
   cook_context : Constr.named_context option;