diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /library/declare.mli | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
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 |