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, 10 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3be72f3fd..3e7d8a9bd 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -13,15 +13,9 @@ open Sign
 
 (*s Constants (internal representation) (Definition/Axiom) *)
 
-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; (* New: younger hyp at top *)
   const_constraints : constraints;
@@ -31,12 +25,10 @@ val is_defined : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
-val cook_constant : constant_value -> constr
-
 (*s Constant declaration. *)
 
 type constant_entry = {
-  const_entry_body : lazy_constant_value;
+  const_entry_body : constr;
   const_entry_type : constr option }
 
 (*s Inductive types (internal representation). *)