modules Instantiate, Constant et Inductive

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

1 files changed, 33 insertions, 0 deletions

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