Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

1 files changed, 1 insertions, 5 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c32bdb85d6..df60899b95 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1851,11 +1851,7 @@ and compile_named env sigma univ auxdefs id =
       Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
 
 let compile_constant env sigma prefix ~interactive con cb =
-     let no_univs =
-       match cb.const_universes with
-       | Monomorphic_const _ -> true
-       | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0
-     in
+    let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in
     begin match cb.const_body with
     | Def t ->
       let t = Mod_subst.force_constr t in