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

(limited to 'kernel/nativecode.ml')

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