diff options
| author | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 09:57:09 +0100 |
| commit | d87c4c472478fbcb30de6efabc68473ee36849a1 (patch) | |
| tree | 5b4e1cb66298db57b978374422822ffdf2673100 /vernac/classes.mli | |
| parent | 850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff) | |
| parent | d00472c59d15259b486868c5ccdb50b6e602a548 (diff) | |
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Diffstat (limited to 'vernac/classes.mli')
| -rw-r--r-- | vernac/classes.mli | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/vernac/classes.mli b/vernac/classes.mli index bb70334342..eb6c0c92e1 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -27,22 +27,22 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit val declare_instance_constant : typeclass -> - Hints.hint_info_expr -> (** priority *) - bool -> (** globality *) - Impargs.manual_explicitation list -> (** implicits *) + Hints.hint_info_expr (** priority *) -> + bool (** globality *) -> + Impargs.manual_explicitation list (** implicits *) -> ?hook:(GlobRef.t -> unit) -> - Id.t -> (** name *) + Id.t (** name *) -> UState.universe_decl -> - bool -> (* polymorphic *) - Evd.evar_map -> (* Universes *) - Constr.t -> (** body *) - Constr.types -> (** type *) + bool (** polymorphic *) -> + Evd.evar_map (** Universes *) -> + Constr.t (** body *) -> + Constr.types (** type *) -> unit val new_instance : - ?abstract:bool -> (** Not abstract by default. *) - ?global:bool -> (** Not global by default. *) - ?refine:bool -> (** Allow refinement *) + ?abstract:bool (** Not abstract by default. *) -> + ?global:bool (** Not global by default. *) -> + ?refine:bool (** Allow refinement *) -> program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> |