diff options
Diffstat (limited to 'toplevel/classes.mli')
| -rw-r--r-- | toplevel/classes.mli | 46 |
1 files changed, 20 insertions, 26 deletions
diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 69e4dd8b..68a93a74 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Names open Decl_kinds open Term @@ -22,59 +19,56 @@ 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 existing_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 -> + constr_expr option -> ?generalize:bool -> ?tac:Proof_type.tactic -> ?hook:(Libnames.global_reference -> unit) -> int option -> identifier -(* Setting opacity *) +(** Setting opacity *) -val set_typeclass_transparency : evaluable_global_reference -> bool -> unit +val set_typeclass_transparency : evaluable_global_reference -> bool -> 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 +val context : local_binder list -> unit -(* Forward ref for refine *) +(** Forward ref for refine *) val refine_ref : (open_constr -> Proof_type.tactic) ref - |