Lazy experimentale temporaire...

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

1 files changed, 5 insertions, 2 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 1abe65c20d..aabefe6bf2 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -81,7 +81,7 @@ let infer_declaration env dcl =
   | DefinitionEntry c ->
       let (j,cst) = infer env c.const_entry_body in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
-      Some j.uj_val, typ, cst, c.const_entry_opaque
+      Some (Lazy.lazy_from_val j.uj_val), typ, cst, c.const_entry_opaque
   | ParameterEntry t ->
       let (j,cst) = infer env t in
       None, Typeops.assumption_of_judgment env j, cst, false
@@ -90,7 +90,10 @@ let build_constant_declaration env (body,typ,cst,op) =
   let ids = match body with 
     | None -> global_vars_set env typ
     | Some b ->
-        Idset.union (global_vars_set env b) (global_vars_set env typ) in
+        Idset.union 
+	  (global_vars_set env (Lazy.force_val b)) 
+	  (global_vars_set env typ) 
+  in
   let hyps = keep_hyps env ids in
     { const_body = body;
       const_type = typ;