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.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'kernel/cbytegen.ml')

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*)
-- 
cgit v1.2.3