1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: typeclasses_errors.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
25
type contexts = Parameters | Properties
27
type typeclass_error =
29
| UnboundMethod of global_reference * identifier located (* Class name, method *)
30
| NoInstance of identifier located * constr list
31
| UnsatisfiableConstraints of evar_defs * (evar_info * hole_kind) option
32
| MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
34
exception TypeClassError of env * typeclass_error
36
val not_a_class : env -> constr -> 'a
38
val unbound_method : env -> global_reference -> identifier located -> 'a
40
val no_instance : env -> identifier located -> constr list -> 'a
42
val unsatisfiable_constraints : env -> evar_defs -> evar option -> 'a
44
val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a