diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 34 |
1 files changed, 26 insertions, 8 deletions
diff --git a/library/declare.mli b/library/declare.mli index 2f1cd06e..12e323f1 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declare.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) +(*i $Id$ i*) (*i*) open Names @@ -21,11 +21,11 @@ open Nametab open Decl_kinds (*i*) -(* This module provides the official functions to declare new variables, +(* 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 such as + reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) open Nametab @@ -34,7 +34,7 @@ open Nametab type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *) + | SectionLocalAssum of types * bool (* Implicit status *) type variable_declaration = dir_path * section_variable_entry * logical_kind @@ -48,6 +48,11 @@ type constant_declaration = constant_entry * logical_kind (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) +type internal_flag = + | KernelVerbose + | KernelSilent + | UserVerbose + val declare_constant : identifier -> constant_declaration -> constant @@ -57,9 +62,22 @@ val declare_internal_constant : (* [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block (boolean must be true iff it is a record) *) -val declare_mind : bool -> mutual_inductive_entry -> object_name +val declare_mind : internal_flag -> mutual_inductive_entry -> object_name -(* hooks for XML output *) +(* Hooks for XML output *) val set_xml_declare_variable : (object_name -> unit) -> unit -val set_xml_declare_constant : (bool * constant -> unit) -> unit -val set_xml_declare_inductive : (bool * object_name -> unit) -> unit +val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit +val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit + +(* Hook for the cache function of constants and inductives *) +val add_cache_hook : (full_path -> unit) -> unit + +(* Declaration messages *) + +val definition_message : identifier -> unit +val assumption_message : identifier -> unit +val fixpoint_message : int array option -> identifier list -> unit +val cofixpoint_message : identifier list -> unit +val recursive_message : bool (* true = fixpoint *) -> + int array option -> identifier list -> unit + |