diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 91 |
1 files changed, 56 insertions, 35 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 456026bf..894333ad 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -1,54 +1,68 @@ (************************************************************************) (* 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 *) (************************************************************************) -open Util open Names open Term open Entries open Libnames +open Globnames open Tacexpr open Vernacexpr -open Topconstr +open Constrexpr open Decl_kinds open Redexpr -open Constrintern open Pfedit (** This file is about the interpretation of raw commands into typed ones and top-level declaration of the main Gallina objects *) +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 + (** {6 Hooks for Pcoq} *) val set_declare_definition_hook : (definition_entry -> unit) -> unit val get_declare_definition_hook : unit -> (definition_entry -> unit) -val set_declare_assumptions_hook : (types -> unit) -> unit (** {6 Definitions/Let} *) val interp_definition : - local_binder list -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * Impargs.manual_implicits + local_binder list -> polymorphic -> red_expr option -> constr_expr -> + constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits -val declare_definition : identifier -> locality * definition_object_kind -> - definition_entry -> Impargs.manual_implicits -> declaration_hook -> unit +val declare_definition : Id.t -> definition_kind -> + definition_entry -> Impargs.manual_implicits -> + Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference + +val do_definition : Id.t -> definition_kind -> + local_binder list -> red_expr option -> constr_expr -> + constr_expr option -> unit Lemmas.declaration_hook -> unit (** {6 Parameters/Assumptions} *) -val interp_assumption : - local_binder list -> constr_expr -> types * Impargs.manual_implicits +(* val interp_assumption : env -> evar_map ref -> *) +(* local_binder list -> constr_expr -> *) +(* types Univ.in_universe_context_set * Impargs.manual_implicits *) -val declare_assumption : coercion_flag -> assumption_kind -> types -> +(** returns [false] if the assumption is neither local to a section, + nor in a module type and meant to be instantiated. *) +val declare_assumption : coercion_flag -> assumption_kind -> + types Univ.in_universe_context_set -> Impargs.manual_implicits -> - bool (** implicit *) -> Entries.inline -> variable located -> unit + bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> + global_reference * Univ.Instance.t * bool + +val do_assumptions : locality * polymorphic * assumption_object_kind -> + Vernacexpr.inline -> simple_binder with_coercion list -> bool -val declare_assumptions : variable located list -> - coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> - bool -> Entries.inline -> unit +(* val declare_assumptions : variable Loc.located list -> *) +(* coercion_flag -> assumption_kind -> types Univ.in_universe_context_set -> *) +(* Impargs.manual_implicits -> bool -> Vernacexpr.inline -> bool *) (** {6 Inductive and coinductive types} *) @@ -56,9 +70,9 @@ val declare_assumptions : variable located list -> inductive declarations *) type structured_one_inductive_expr = { - ind_name : identifier; + ind_name : Id.t; ind_arity : constr_expr; - ind_lc : (identifier * constr_expr) list + ind_lc : (Id.t * constr_expr) list } type structured_inductive_expr = @@ -75,26 +89,28 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : - structured_inductive_expr -> decl_notation list -> bool -> + structured_inductive_expr -> decl_notation list -> polymorphic -> + private_flag -> Decl_kinds.recursivity_kind -> mutual_inductive_entry * one_inductive_impls list (** Registering a mutual inductive definition together with its associated schemes *) val declare_mutual_inductive_with_eliminations : - Declare.internal_flag -> mutual_inductive_entry -> one_inductive_impls list -> + mutual_inductive_entry -> one_inductive_impls list -> mutual_inductive (** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : - (one_inductive_expr * decl_notation list) list -> bool -> unit + (one_inductive_expr * decl_notation list) list -> polymorphic -> + private_flag -> Decl_kinds.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) type structured_fixpoint_expr = { - fix_name : identifier; - fix_annot : identifier located option; + fix_name : Id.t; + fix_annot : Id.t Loc.located option; fix_binders : local_binder list; fix_body : constr_expr option; fix_type : constr_expr @@ -114,37 +130,42 @@ val extract_cofixpoint_components : (** Typing global fixpoints and cofixpoint_expr *) type recursive_preentry = - identifier list * constr option list * types list + Id.t list * constr option list * types list val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * Impargs.manual_implicits * int option) list + recursive_preentry * Evd.evar_universe_context * + (Name.t list * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * Impargs.manual_implicits * int option) list + recursive_preentry * Evd.evar_universe_context * + (Name.t list * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> + locality -> polymorphic -> + recursive_preentry * Evd.evar_universe_context * + (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit -val declare_cofixpoint : - recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> - decl_notation list -> unit +val declare_cofixpoint : locality -> polymorphic -> + recursive_preentry * Evd.evar_universe_context * + (Name.t list * Impargs.manual_implicits * int option) list -> + decl_notation list -> unit (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : - (fixpoint_expr * decl_notation list) list -> unit + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : - (cofixpoint_expr * decl_notation list) list -> unit + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit (** Utils *) -val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit +val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit -val declare_fix : definition_object_kind -> identifier -> - constr -> types -> Impargs.manual_implicits -> global_reference +val declare_fix : definition_kind -> Univ.universe_context -> Id.t -> + Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference |