diff options
| author | Enrico Tassi | 2019-05-24 14:57:33 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:43 +0200 |
| commit | a7a6fa3219134004f1fc6c757f1c16281724f38f (patch) | |
| tree | 3d0653067a9ea3c574b6237f6f8d0c5adae72450 /vernac/classes.mli | |
| parent | d77604cb06fcc8e8f38ef979627aa7a7138ef0f2 (diff) | |
[vernac] more precise types for Add Morph, Instance, and Function
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. *) |