diff options
Diffstat (limited to 'toplevel/classes.mli')
| -rw-r--r-- | toplevel/classes.mli | 52 |
1 files changed, 20 insertions, 32 deletions
diff --git a/toplevel/classes.mli b/toplevel/classes.mli index f3cb0c58..f149ac72 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: classes.mli 11024 2008-05-30 12:41:39Z msozeau $ i*) +(*i $Id: classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Names @@ -23,17 +23,21 @@ open Typeclasses open Implicit_quantifiers (*i*) +(* Errors *) + +val mismatched_params : env -> constr_expr list -> rel_context -> 'a + +val mismatched_props : env -> constr_expr list -> rel_context -> 'a + type binder_list = (identifier located * bool * constr_expr) list type binder_def_list = (identifier located * identifier located list * constr_expr) list val binders_of_lidents : identifier located list -> local_binder list -val declare_implicit_proj : typeclass -> (identifier * constant) -> - Impargs.manual_explicitation list -> bool -> unit -(* -val infer_super_instances : env -> constr list -> - named_context -> named_context -> types list * identifier list * named_context -*) +val name_typeclass_binders : Idset.t -> + Topconstr.local_binder list -> + Topconstr.local_binder list * Idset.t + val new_class : identifier located -> local_binder list -> Vernacexpr.sort_expr located option -> @@ -46,6 +50,10 @@ val default_on_free_vars : identifier list -> unit val fail_on_free_vars : identifier list -> unit +(* Instance declaration *) + +val declare_instance : bool -> identifier located -> unit + val declare_instance_constant : typeclass -> int option -> (* priority *) @@ -69,35 +77,15 @@ val new_instance : identifier (* For generation on names based on classes only *) -val id_of_class : typeclass -> identifier - -val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit - -val declare_instance : bool -> identifier located -> unit -val mismatched_params : env -> constr_expr list -> named_context -> 'a +val id_of_class : typeclass -> identifier -val mismatched_props : env -> constr_expr list -> named_context -> 'a +(* Context command *) -val solve_by_tac : env -> - Evd.evar_defs -> - Evd.evar -> - evar_info -> - Proof_type.tactic -> - Evd.evar_defs * bool +val context : ?hook:(Libnames.global_reference -> unit) -> + local_binder list -> unit -val solve_evars_by_tac : env -> - Evd.evar_defs -> - Proof_type.tactic -> - Evd.evar_defs +(* Forward ref for refine *) val refine_ref : (open_constr -> Proof_type.tactic) ref -val decompose_named_assum : types -> named_context * types - -val push_named_context : named_context -> env -> env - -val name_typeclass_binders : Idset.t -> - Topconstr.local_binder list -> - Topconstr.local_binder list * Idset.t - |