From ece55632bef1eb61cd557ec8d93986c60aef7b58 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Sep 2002 07:19:30 +0000
Subject: Que des niveaux d'univers frais dans le type des constantes globales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3043 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 01b883998f..a6e42a73a4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -72,8 +72,9 @@ let constant_entry_of_com (bl,com,comtypopt,opacity) =
   match comtypopt with
       None -> 
 	let b = abstract_rawconstr com bl in
-	{ const_entry_body = interp_constr sigma env b;
-	  const_entry_type = None;
+	let j = judgment_of_rawconstr sigma env b in
+	{ const_entry_body = j.uj_val;
+	  const_entry_type = Some (Evarutil.refresh_universes j.uj_type);
           const_entry_opaque = opacity }
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
-- 
cgit v1.2.3