diff options
Diffstat (limited to 'library/declare.mli')
| -rw-r--r-- | library/declare.mli | 63 |
1 files changed, 35 insertions, 28 deletions
diff --git a/library/declare.mli b/library/declare.mli index 2de128bd..03b66271 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,12 +9,7 @@ open Names open Libnames open Term -open Sign -open Declarations open Entries -open Indtypes -open Safe_typing -open Nametab open Decl_kinds (** This module provides the official functions to declare new variables, @@ -24,15 +19,13 @@ open Decl_kinds reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) -open Nametab - (** 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 definition_entry + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) -type variable_declaration = dir_path * section_variable_entry * logical_kind +type variable_declaration = DirPath.t * section_variable_entry * logical_kind val declare_variable : variable -> variable_declaration -> object_name @@ -54,29 +47,43 @@ type internal_flag = | KernelSilent | UserVerbose +(* Defaut definition entries, transparent with no secctx or proj information *) +val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> + ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects -> + constr -> definition_entry + val declare_constant : - ?internal:internal_flag -> identifier -> constant_declaration -> constant + ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> 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 : internal_flag -> mutual_inductive_entry -> object_name +val declare_definition : + ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> + ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> + constr Univ.in_universe_context_set -> constant -(** 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 +(** Since transparent constant's side effects are globally declared, we + * need that *) +val set_declare_scheme : + (string -> (inductive * constant) array -> unit) -> unit -(** Hook for the cache function of constants and inductives *) -val add_cache_hook : (full_path -> unit) -> unit +(** [declare_mind me] declares a block of inductive types with + their constructors in the current section; it returns the path of + the whole block and a boolean indicating if it is a primitive record. *) +val declare_mind : mutual_inductive_entry -> object_name * bool (** 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 definition_message : Id.t -> unit +val assumption_message : Id.t -> unit +val fixpoint_message : int array option -> Id.t list -> unit +val cofixpoint_message : Id.t list -> unit val recursive_message : bool (** true = fixpoint *) -> - int array option -> identifier list -> unit + int array option -> Id.t list -> unit + +val exists_name : Id.t -> bool + + + +(** Global universe names and constraints *) -val exists_name : identifier -> bool +val do_universe : Id.t Loc.located list -> unit +val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit |