nouveau discharge fait par le noyau; plus de recettes dans les corps des constantes

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

1 files changed, 2 insertions, 12 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ff80c338f9..96eef57001 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -8,15 +8,9 @@ open Sign
 
 (* Constant entries *)
 
-type lazy_constant_value =
-  | Cooked of constr
-  | Recipe of (unit -> constr)
-
-type constant_value = lazy_constant_value ref
-
 type constant_body = {
   const_kind : path_kind;
-  const_body : constant_value option;
+  const_body : constr option;
   const_type : types;
   const_hyps : named_context;
   const_constraints : constraints;
@@ -27,12 +21,8 @@ let is_defined cb =
 
 let is_opaque cb = cb.const_opaque
 
-let cook_constant = function
-  | { contents = Cooked c } -> c
-  | { contents = Recipe f } as v -> let c = f () in v := Cooked c; c
-
 type constant_entry = {
-  const_entry_body : lazy_constant_value;
+  const_entry_body : constr;
   const_entry_type : constr option }
 
 (* Inductive entries *)