summaryrefslogtreecommitdiff
path: root/toplevel/command.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/command.mli')
-rw-r--r--toplevel/command.mli91
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 00:14:13 +0000