1 files changed, 25 insertions, 0 deletions
diff --git a/library/declare.mli b/library/declare.mli
new file mode 100644
index 000000000..21486c250
--- /dev/null
+++ b/library/declare.mli
@@ -0,0 +1,25 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Constant
+open Inductive
+(*i*)
+
+(* This module provides the official functions to declare new variables, 
+   parameters, constants and inductive types. Using the following functions
+   will add the entries in the global environment (module [Global]), will
+   register the declarations in the library (module [Lib]) --- so that the
+   reset works properly --- and will fill some global tables as [Nametab] and
+   [Impargs]. *)
+
+val declare_variable : identifier -> constr -> unit
+
+val declare_parameter : identifier -> constr -> unit
+
+val declare_constant : identifier -> constant_entry -> unit
+
+val declare_mind : mutual_inductive_entry -> unit
+