From feabced9caa5996738d1c51fec8428623ebf0fd6 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 18 Aug 1999 15:20:08 +0000
Subject: module Reduction (fin)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/constant.mli | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

(limited to 'kernel/constant.mli')

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