diff options
| author | Maxime Dénès | 2019-06-05 10:11:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-06-05 10:11:26 +0200 |
| commit | c0a695e89b0562eb6450c04ddba5e6e0414e5fd8 (patch) | |
| tree | 376928f87987f440142cc7e6353c6987cb4b2be7 /vernac/classes.mli | |
| parent | 658ae0d320473e25ee60cf158ed808be294f3a69 (diff) | |
| parent | ae87619019adf56acf8985f7f1c4e49246ca9b5a (diff) | |
Merge PR #10215: Refine typing of vernacular commands
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 43 |
1 files changed, 25 insertions, 18 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index 8d5f3e3a06..e61935c87a 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -31,34 +31,41 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map -> val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) -val declare_instance_constant : - typeclass -> - Hints.hint_info_expr (** priority *) -> - bool (** globality *) -> - Impargs.manual_explicitation list (** implicits *) -> - ?hook:(GlobRef.t -> unit) -> - Id.t (** name *) -> - UState.universe_decl -> - bool (** polymorphic *) -> - Evd.evar_map (** Universes *) -> - Constr.t (** body *) -> - Constr.types (** type *) -> - unit +val new_instance_interactive : + ?global:bool (** Not global by default. *) + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> ?generalize:bool + -> ?tac:unit Proofview.tactic + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t * Proof_global.t val new_instance : - pstate:Proof_global.t option - -> ?global:bool (** Not global by default. *) - -> program_mode:bool + ?global:bool (** Not global by default. *) + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> (bool * constr_expr) + -> ?generalize:bool + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t + +val new_instance_program : + ?global:bool (** Not global by default. *) -> Decl_kinds.polymorphic -> name_decl -> local_binder_expr list -> constr_expr -> (bool * constr_expr) option -> ?generalize:bool - -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr - -> Id.t * Proof_global.t option (* May open a proof *) + -> Id.t val declare_new_instance : ?global:bool (** Not global by default. *) |