diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 78 |
1 files changed, 35 insertions, 43 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index af89b59a..8ffdbdec 100644 --- a/toplevel/command.mli +++ b/toplevel/command.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: command.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Term @@ -21,45 +18,41 @@ open Decl_kinds open Redexpr open Constrintern open Pfedit -(*i*) -(*s This file is about the interpretation of raw commands into typed +(** This file is about the interpretation of raw commands into typed ones and top-level declaration of the main Gallina objects *) -(* Hooks for Pcoq *) +(** {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 -(*************************************************************************) -(* Definitions/Let *) +(** {6 Definitions/Let} *) val interp_definition : - boxed_flag -> local_binder list -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * manual_implicits + local_binder list -> red_expr option -> constr_expr -> + constr_expr option -> definition_entry * Impargs.manual_implicits val declare_definition : identifier -> locality * definition_object_kind -> - definition_entry -> manual_implicits -> declaration_hook -> unit + definition_entry -> Impargs.manual_implicits -> declaration_hook -> unit -(*************************************************************************) -(* Parameters/Assumptions *) +(** {6 Parameters/Assumptions} *) val interp_assumption : - local_binder list -> constr_expr -> types * manual_implicits + local_binder list -> constr_expr -> types * Impargs.manual_implicits val declare_assumption : coercion_flag -> assumption_kind -> types -> - manual_implicits -> - bool (* implicit *) -> bool (* inline *) -> variable located -> unit + Impargs.manual_implicits -> + bool (** implicit *) -> Entries.inline -> variable located -> unit val declare_assumptions : variable located list -> - coercion_flag -> assumption_kind -> types -> manual_implicits -> - bool -> bool -> unit + coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits -> + bool -> Entries.inline -> unit -(*************************************************************************) -(* Inductive and coinductive types *) +(** {6 Inductive and coinductive types} *) -(* Extracting the semantical components out of the raw syntax of mutual +(** Extracting the semantical components out of the raw syntax of mutual inductive declarations *) type structured_one_inductive_expr = { @@ -75,30 +68,29 @@ val extract_mutual_inductive_declaration_components : (one_inductive_expr * decl_notation list) list -> structured_inductive_expr * (*coercions:*) qualid list * decl_notation list -(* Typing mutual inductive definitions *) +(** Typing mutual inductive definitions *) type one_inductive_impls = - Impargs.manual_explicitation list (* for inds *)* - Impargs.manual_explicitation list list (* for constrs *) + Impargs.manual_implicits (** for inds *)* + Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> bool -> mutual_inductive_entry * one_inductive_impls list -(* Registering a mutual inductive definition together with its +(** 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 points for the vernacular commands Inductive and CoInductive *) +(** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> bool -> unit -(*************************************************************************) -(* Fixpoints and cofixpoints *) +(** {6 Fixpoints and cofixpoints} *) type structured_fixpoint_expr = { fix_name : identifier; @@ -108,10 +100,10 @@ type structured_fixpoint_expr = { fix_type : constr_expr } -(* Extracting the semantical components out of the raw syntax of +(** Extracting the semantical components out of the raw syntax of (co)fixpoints declarations *) -val extract_fixpoint_components : +val extract_fixpoint_components : bool -> (fixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list @@ -119,40 +111,40 @@ val extract_cofixpoint_components : (cofixpoint_expr * decl_notation list) list -> structured_fixpoint_expr list * decl_notation list -(* Typing global fixpoints and cofixpoint_expr *) +(** Typing global fixpoints and cofixpoint_expr *) type recursive_preentry = identifier list * constr option list * types list val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * manual_implicits * int option) list + recursive_preentry * (name list * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (name list * manual_implicits * int option) list + recursive_preentry * (name list * Impargs.manual_implicits * int option) list -(* Registering fixpoints and cofixpoints in the environment *) +(** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - bool -> recursive_preentry * (name list * manual_implicits * int option) list -> + recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : - bool -> recursive_preentry * (name list * manual_implicits * int option) list -> + recursive_preentry * (name list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit -(* Entry points for the vernacular commands Fixpoint and CoFixpoint *) +(** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : - (fixpoint_expr * decl_notation list) list -> bool -> unit + (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : - (cofixpoint_expr * decl_notation list) list -> bool -> unit + (cofixpoint_expr * decl_notation list) list -> unit -(* Utils *) +(** Utils *) val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit -val declare_fix : bool -> definition_object_kind -> identifier -> - constr -> types -> Impargs.manual_explicitation list -> global_reference +val declare_fix : definition_object_kind -> identifier -> + constr -> types -> Impargs.manual_implicits -> global_reference |