diff options
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 29 |
1 files changed, 28 insertions, 1 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index daba78217b..9572cd9598 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -31,6 +31,19 @@ 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 new_instance_interactive : + ?global:bool (** Not global by default. *) + -> program_mode:bool + -> 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 : ?global:bool (** Not global by default. *) -> program_mode:bool @@ -38,12 +51,26 @@ val new_instance : -> name_decl -> local_binder_expr list -> constr_expr + -> (bool * constr_expr) + -> ?generalize:bool + -> ?tac:unit Proofview.tactic + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t + +val new_instance_program : + ?global:bool (** Not global by default. *) + -> program_mode:bool + -> 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. *) |