From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 kernel/cbytegen.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/cbytegen.ml')

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 57b397e6f8..02c6a2c715 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -992,8 +992,8 @@ let compile_constant_body fail_on_error env univs = function
       let body = Mod_subst.force_constr sb in
       let instance_size =
         match univs with
-        | None -> 0
-        | Some univ -> Univ.UContext.size univ
+        | Monomorphic_const _ -> 0
+        | Polymorphic_const univ -> Univ.AUContext.size univ
       in
       match kind_of_term body with
 	| Const (kn',u) when is_univ_copy instance_size u ->
-- 
cgit v1.2.3