diff options
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
| -rw-r--r-- | pretyping/typeclasses_errors.ml | 34 |
1 files changed, 5 insertions, 29 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index da5dc909..4f88dd86 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,26 +8,19 @@ (*i*) open Names -open Decl_kinds open Term -open Sign +open Context open Evd open Environ -open Nametab -open Mod_subst -open Topconstr -open Compat -open Util -open Libnames +open Constrexpr +open Globnames (*i*) type contexts = Parameters | Properties type typeclass_error = | NotAClass of constr - | UnboundMethod of global_reference * identifier located (* Class name, method *) - | NoInstance of identifier located * constr list - | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option + | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *) | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *) exception TypeClassError of env * typeclass_error @@ -38,21 +31,4 @@ let not_a_class env c = typeclass_error env (NotAClass c) let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id)) -let no_instance env id args = typeclass_error env (NoInstance (id, args)) - -let unsatisfiable_constraints env evd ev = - match ev with - | None -> - raise (TypeClassError (env, UnsatisfiableConstraints (evd, None))) - | Some ev -> - let loc, kind = Evd.evar_source ev evd in - raise (Loc.Exc_located (loc, TypeClassError - (env, UnsatisfiableConstraints (evd, Some (ev, kind))))) - let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) - -let rec unsatisfiable_exception exn = - match exn with - | TypeClassError (_, UnsatisfiableConstraints _) -> true - | Loc.Exc_located(_, e) -> unsatisfiable_exception e - | _ -> false |