module Reduction (fin)

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

1 files changed, 17 insertions, 1 deletions

diff --git a/kernel/constant.mli b/kernel/constant.mli
index 5c6fb0d139..4de51f8593 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -1,4 +1,20 @@
 
 (* $Id$ *)
 
-type constant
+open Names
+open Term
+
+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_type : type_judgment;
+  mutable const_eval : ((int * constr) list * int * bool) option option;
+}
+
+type constant_entry = section_path * constant_body