4 files changed, 11 insertions, 28 deletions
diff --git a/kernel/constant.ml b/kernel/constant.ml
index 39eda93fc1..c93d486faa 100644
--- a/kernel/constant.ml
+++ b/kernel/constant.ml
@@ -7,23 +7,13 @@ open Generic
 open Term
 open Sign
 
-type discharge_recipe = {
-  d_expand : section_path list;
-  d_modify : (sorts oper * sorts oper modification) list;
-  d_abstract : identifier list;
-  d_from : section_path }
-
-type recipe =
-  | Cooked of constr
-  | Recipe of discharge_recipe
-
 type constant_entry = {
   const_entry_body : constr;
   const_entry_type : constr option }
 
 type constant_body = {
   const_kind : path_kind;
-  const_body : recipe ref option;
+  const_body : constr option;
   const_type : typed_type;
   const_hyps : typed_type signature;
   const_constraints : constraints;
diff --git a/kernel/constant.mli b/kernel/constant.mli
index d9adc6d751..800f95811c 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -10,15 +10,9 @@ open Sign
 
 (* Constants (internal representation). *)
 
-type discharge_recipe
-
-type recipe =
-  | Cooked of constr
-  | Recipe of discharge_recipe
-
 type constant_body = {
   const_kind : path_kind;
-  const_body : recipe ref option;
+  const_body : constr option;
   const_type : typed_type;
   const_hyps : typed_type signature;
   const_constraints : constraints;
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 679789d6ce..e1f9356df8 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -42,15 +42,14 @@ let constant_value env k =
   let cb = lookup_constant sp env in
   if not cb.const_opaque & defined_constant env k then
     match cb.const_body with
-      Some { contents = Cooked body } -> 
-        instantiate_constr 
-	  (ids_of_sign cb.const_hyps) body (Array.to_list args)
-    | Some { contents = Recipe _ } ->
-        anomalylabstrm "termenv__constant_value"
-          [< 'sTR "a transparent constant which was not cooked" >]
-    | None -> anomalylabstrm "termenv__constant_value"
-          [< 'sTR "a defined constant as no body." >]
-  else failwith "opaque"
+      | Some body -> 
+          instantiate_constr 
+	    (ids_of_sign cb.const_hyps) body (Array.to_list args)
+      | None -> 
+	  anomalylabstrm "termenv__constant_value"
+	    [< 'sTR "a defined constant as no body." >]
+  else 
+    failwith "opaque"
 
 let const_abst_opt_value env c =
   match c with
diff --git a/kernel/typing.ml b/kernel/typing.ml
index 896d469c8c..071403d628 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -284,7 +284,7 @@ let add_constant sp ce env =
   in
   let cb = { 
     const_kind = kind_of_path sp;
-    const_body = Some (ref (Cooked ce.const_entry_body));
+    const_body = Some ce.const_entry_body;
     const_type = ty;
     const_hyps = get_globals (context env);
     const_constraints = Constraint.union cst cst';