1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: declare.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
24
(* This module provides the official functions to declare new variables,
25
parameters, constants and inductive types. Using the following functions
26
will add the entries in the global environment (module [Global]), will
27
register the declarations in the library (module [Lib]) --- so that the
28
reset works properly --- and will fill some global tables such as
29
[Nametab] and [Impargs]. *)
33
(* Declaration of local constructions (Variable/Hypothesis/Local) *)
35
type section_variable_entry =
36
| SectionLocalDef of constr * types option * bool (* opacity *)
37
| SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep list *)
39
type variable_declaration = dir_path * section_variable_entry * logical_kind
41
val declare_variable : variable -> variable_declaration -> object_name
43
(* Declaration of global constructions *)
44
(* i.e. Definition/Theorem/Axiom/Parameter/... *)
46
type constant_declaration = constant_entry * logical_kind
48
(* [declare_constant id cd] declares a global declaration
49
(constant/parameter) with name [id] in the current section; it returns
50
the full path of the declaration *)
51
val declare_constant :
52
identifier -> constant_declaration -> constant
54
val declare_internal_constant :
55
identifier -> constant_declaration -> constant
57
(* [declare_mind me] declares a block of inductive types with
58
their constructors in the current section; it returns the path of
59
the whole block (boolean must be true iff it is a record) *)
60
val declare_mind : bool -> mutual_inductive_entry -> object_name
62
(* hooks for XML output *)
63
val set_xml_declare_variable : (object_name -> unit) -> unit
64
val set_xml_declare_constant : (bool * constant -> unit) -> unit
65
val set_xml_declare_inductive : (bool * object_name -> unit) -> unit