diff options
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index f80dbb9897..d441fd342c 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -32,8 +32,7 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val new_instance : - pstate:Proof_global.t option - -> ?global:bool (** Not global by default. *) + ?global:bool (** Not global by default. *) -> program_mode:bool -> Decl_kinds.polymorphic -> name_decl @@ -44,7 +43,7 @@ val new_instance : -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr - -> Id.t * Proof_global.t option (* May open a proof *) + -> Id.t * Proof_global.pstate option (* May open a proof *) val declare_new_instance : ?global:bool (** Not global by default. *) |