From 723c344d3e4cf7fdc2e4854ea7d55d140570424d Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 6 Nov 2000 16:43:51 +0000
Subject: 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
---
 kernel/declarations.ml | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

(limited to 'kernel/declarations.ml')

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 *)
-- 
cgit v1.2.3