Que des niveaux d'univers frais dans le type des constantes globales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3045 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 12 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index a6e42a73a4..a670c2bda2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -354,14 +354,11 @@ let build_recursive lnameargsardef =
   let n = NeverDischarge in 
   let recvec = 
     Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
+  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
   let rec declare i fi =
     let ce = 
-      { const_entry_body =
-	  mkFix ((nvrec,i),
-	         (Array.map (fun id -> Name id) namerec,
-                  arrec,
-		  recvec));
-        const_entry_type = None;
+      { const_entry_body = mkFix ((nvrec,i),recdecls);
+        const_entry_type = Some arrec.(i);
         const_entry_opaque = false } in
     let (_,kn) = declare_constant fi (DefinitionEntry ce, n) in
     (ConstRef kn)
@@ -418,13 +415,11 @@ let build_corecursive lnameardef =
   let n = NeverDischarge in 
   let recvec = 
     Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
+  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
   let rec declare i fi =
     let ce = 
-      { const_entry_body =
-	  mkCoFix (i, (Array.map (fun id -> Name id) namerec,
-                       arrec,
-		       recvec));
-        const_entry_type = None;
+      { const_entry_body = mkCoFix (i, recdecls);
+        const_entry_type = Some (arrec.(i));
         const_entry_opaque = false } 
     in
     let _,kn = declare_constant fi (DefinitionEntry ce,n) in
@@ -462,8 +457,10 @@ let build_scheme lnamedepindsort =
   let n = NeverDischarge in 
   let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
   let rec declare decl fi lrecref =
+    let decltype = Retyping.get_type_of env0 Evd.empty decl in
+    let decltype = Evarutil.refresh_universes decltype in
     let ce = { const_entry_body = decl;
-               const_entry_type = None;
+               const_entry_type = Some decltype;
                const_entry_opaque = false } in
     let _,kn = declare_constant fi (DefinitionEntry ce,n) in
     ConstRef kn :: lrecref