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/cbytegen.ml b/kernel/cbytegen.ml
index b95a940c14..718584b3d4 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -881,11 +881,7 @@ let compile_constant_body ~fail_on_error env univs = function
   | Undef _ | OpaqueDef _ | Primitive _ -> Some BCconstant
   | Def sb ->
       let body = Mod_subst.force_constr sb in
-      let instance_size =
-        match univs with
-        | Monomorphic_const _ -> 0
-        | Polymorphic_const univ -> Univ.AUContext.size univ
-      in
+      let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in
       match kind body with
 	| Const (kn',u) when is_univ_copy instance_size u ->
 	    (* we use the canonical name of the constant*)