diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 42 |
1 files changed, 28 insertions, 14 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index d2ebdc561..b2ba23ef2 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -29,7 +29,7 @@ val get_declare_definition_hook : unit -> (definition_entry -> unit) (** {6 Definitions/Let} *) val interp_definition : - local_binder list -> red_expr option -> constr_expr -> + local_binder list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits val declare_definition : Id.t -> definition_kind -> @@ -42,16 +42,25 @@ val do_definition : Id.t -> definition_kind -> (** {6 Parameters/Assumptions} *) +(* val interp_assumption : env -> evar_map ref -> *) +(* local_binder list -> constr_expr -> *) +(* types Univ.in_universe_context_set * Impargs.manual_implicits *) + (** 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 -> +val declare_assumption : coercion_flag -> assumption_kind -> + types Univ.in_universe_context_set -> Impargs.manual_implicits -> bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> global_reference * bool -val do_assumptions : locality * assumption_object_kind -> +val do_assumptions : locality * polymorphic * assumption_object_kind -> Vernacexpr.inline -> simple_binder with_coercion list -> bool +(* 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} *) (** Extracting the semantical components out of the raw syntax of mutual @@ -77,7 +86,7 @@ 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 -> bool(*finite*) -> mutual_inductive_entry * one_inductive_impls list (** Registering a mutual inductive definition together with its @@ -90,7 +99,7 @@ val declare_mutual_inductive_with_eliminations : (** 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 -> bool -> unit (** {6 Fixpoints and cofixpoints} *) @@ -120,33 +129,38 @@ type recursive_preentry = val interp_fixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list + recursive_preentry * Univ.universe_context_set * + (Name.t list * Impargs.manual_implicits * int option) list val interp_cofixpoint : structured_fixpoint_expr list -> decl_notation list -> - recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list + recursive_preentry * Univ.universe_context_set * + (Name.t list * Impargs.manual_implicits * int option) list (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - locality -> recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list -> + locality -> polymorphic -> + recursive_preentry * Univ.universe_context_set * + (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit -val declare_cofixpoint : - locality -> recursive_preentry * (Name.t list * Impargs.manual_implicits * int option) list -> - decl_notation list -> unit +val declare_cofixpoint : locality -> polymorphic -> + recursive_preentry * Univ.universe_context_set * + (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 : - locality -> (fixpoint_expr * decl_notation list) list -> unit + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : - locality -> (cofixpoint_expr * decl_notation list) list -> unit + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit (** Utils *) val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit -val declare_fix : definition_kind -> Id.t -> +val declare_fix : definition_kind -> Univ.universe_context -> Id.t -> Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference |