From 979451471e37a76ce15e45f7b174a49cbb73f9ae Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 25 Aug 1999 14:12:43 +0000
Subject: modules Instantiate, Constant et Inductive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@22 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/constant.ml | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 kernel/constant.ml

(limited to 'kernel/constant.ml')

diff --git a/kernel/constant.ml b/kernel/constant.ml
new file mode 100644
index 0000000000..0b52af6956
--- /dev/null
+++ b/kernel/constant.ml
@@ -0,0 +1,33 @@
+
+(* $Id$ *)
+
+open Names
+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_body = {
+  const_kind : path_kind;
+  const_body : recipe ref option;
+  const_type : typed_type;
+  const_hyps : context;
+  mutable const_opaque : bool;
+  mutable const_eval : ((int * constr) list * int * bool) option option;
+}
+
+type constant_entry = section_path * constant_body
+
+let is_defined cb = 
+  match cb.const_body with Some _ -> true | _ -> false
+
+let is_opaque cb = cb.const_opaque
-- 
cgit v1.2.3