diff options
Diffstat (limited to 'toplevel/classes.mli')
| -rw-r--r-- | toplevel/classes.mli | 46 |
1 files changed, 22 insertions, 24 deletions
diff --git a/toplevel/classes.mli b/toplevel/classes.mli index b8b104d47..279622843 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -1,14 +1,13 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Names open Decl_kinds open Term @@ -22,36 +21,35 @@ open Util open Typeclasses open Implicit_quantifiers open Libnames -(*i*) -(* Errors *) +(** Errors *) val mismatched_params : env -> constr_expr list -> rel_context -> 'a val mismatched_props : env -> constr_expr list -> rel_context -> 'a -(* Post-hoc class declaration. *) +(** Post-hoc class declaration. *) val declare_class : reference -> unit -(* Instance declaration *) +(** Instance declaration *) val declare_instance : bool -> reference -> unit val declare_instance_constant : typeclass -> - int option -> (* priority *) - bool -> (* globality *) - Impargs.manual_explicitation list -> (* implicits *) + int option -> (** priority *) + bool -> (** globality *) + Impargs.manual_explicitation list -> (** implicits *) ?hook:(Libnames.global_reference -> unit) -> - identifier -> (* name *) - Term.constr -> (* body *) - Term.types -> (* type *) + identifier -> (** name *) + Term.constr -> (** body *) + Term.types -> (** type *) Names.identifier val new_instance : - ?abstract:bool -> (* Not abstract by default. *) - ?global:bool -> (* Not global by default. *) + ?abstract:bool -> (** Not abstract by default. *) + ?global:bool -> (** Not global by default. *) local_binder list -> typeclass_constraint -> constr_expr -> @@ -61,20 +59,20 @@ val new_instance : int option -> identifier -(* Setting opacity *) +(** Setting opacity *) val set_typeclass_transparency : evaluable_global_reference -> bool -> unit -(* For generation on names based on classes only *) +(** For generation on names based on classes only *) val id_of_class : typeclass -> identifier -(* Context command *) +(** Context command *) val context : ?hook:(Libnames.global_reference -> unit) -> local_binder list -> unit -(* Forward ref for refine *) +(** Forward ref for refine *) val refine_ref : (open_constr -> Proof_type.tactic) ref |