diff options
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index 7e0ec42625..73e4b024ef 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -40,6 +40,7 @@ val declare_instance_constant : unit val new_instance : + pstate:Proof_global.t option -> ?global:bool (** Not global by default. *) -> ?refine:bool (** Allow refinement *) -> program_mode:bool -> @@ -51,7 +52,8 @@ val new_instance : ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr -> - Id.t + (* May open a proof *) + Id.t * Proof_global.t option val declare_new_instance : ?global:bool (** Not global by default. *) -> @@ -74,4 +76,8 @@ val id_of_class : typeclass -> Id.t (** returns [false] if, for lack of section, it declares an assumption (unless in a module type). *) -val context : Decl_kinds.polymorphic -> local_binder_expr list -> bool +val context + : pstate:Proof_global.t option + -> Decl_kinds.polymorphic + -> local_binder_expr list + -> bool |