diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 43 |
1 files changed, 21 insertions, 22 deletions
diff --git a/library/declare.mli b/library/declare.mli index 1ada7cc9..61c19996 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declare.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Libnames open Term @@ -19,9 +16,8 @@ open Indtypes open Safe_typing 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 @@ -30,54 +26,57 @@ open Decl_kinds open Nametab -(* Declaration of local constructions (Variable/Hypothesis/Local) *) +(** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = - | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types * bool (* Implicit status *) + | SectionLocalDef of constr * types option * bool (** opacity *) + | SectionLocalAssum of types * bool (** Implicit status *) type variable_declaration = dir_path * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> object_name -(* Declaration of global constructions *) -(* i.e. Definition/Theorem/Axiom/Parameter/... *) +(** Declaration of global constructions + i.e. Definition/Theorem/Axiom/Parameter/... *) type constant_declaration = constant_entry * logical_kind -(* [declare_constant id cd] declares a global declaration +(** [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 *) + the full path of the declaration + + internal specify if the constant has been created by the kernel or by the + user, and in the former case, if its errors should be silent + + *) type internal_flag = | KernelVerbose | KernelSilent | UserVerbose val declare_constant : - identifier -> constant_declaration -> constant - -val declare_internal_constant : - identifier -> constant_declaration -> constant + ?internal:internal_flag -> identifier -> constant_declaration -> constant -(* [declare_mind me] declares a block of inductive types with +(** [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 : 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 : (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 *) +(** Hook for the cache function of constants and inductives *) val add_cache_hook : (full_path -> unit) -> unit -(* Declaration messages *) +(** 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 *) -> +val recursive_message : bool (** true = fixpoint *) -> int array option -> identifier list -> unit +val exists_name : identifier -> bool |