From 00d32afd7c6b270bab55671d7a5aeff125a1ca29 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Fri, 21 Nov 2014 00:41:53 +0100
Subject: Fix bug #3804.

---
 kernel/modops.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index ccec3c170..05eac6221 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -353,9 +353,14 @@ let strengthen_const mp_from l cb resolver =
   |_ ->
     let kn = KerName.make2 mp_from l in
     let con = constant_of_delta_kn resolver kn in
-    { cb with
-      const_body = Def (Mod_subst.from_val (mkConst con));
-      const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) }
+    let u = 
+      if cb.const_polymorphic then 
+	Univ.UContext.instance cb.const_universes
+      else Univ.Instance.empty
+    in
+      { cb with
+	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
+	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then mb
-- 
cgit v1.2.3