diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /pretyping/typeclasses_errors.ml | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
-rw-r--r-- | pretyping/typeclasses_errors.ml | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml new file mode 100644 index 00000000..9faac94d --- /dev/null +++ b/pretyping/typeclasses_errors.ml @@ -0,0 +1,55 @@ +(************************************************************************) +(* 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: typeclasses_errors.ml 11150 2008-06-19 11:38:27Z msozeau $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Topconstr +open Util +open Libnames +(*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_defs * (evar_info * hole_kind) option + | MismatchedContextInstance of contexts * constr_expr list * named_context (* found, expected *) + +exception TypeClassError of env * typeclass_error + +let typeclass_error env err = raise (TypeClassError (env, err)) + +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 = + let evd = Evd.undefined_evars evd in + match ev with + | None -> + raise (TypeClassError (env, UnsatisfiableConstraints (evd, None))) + | Some ev -> + let evi = Evd.find (Evd.evars_of evd) ev in + let loc, kind = Evd.evar_source ev evd in + raise (Stdpp.Exc_located (loc, TypeClassError + (env, UnsatisfiableConstraints (evd, Some (evi, kind))))) + +let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) |