diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-15 20:48:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-27 22:35:10 +0200 |
| commit | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (patch) | |
| tree | 78c30edd51e65c8e7014ac360c5027da77ff20b2 /pretyping/evarsolve.ml | |
| parent | 2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff) | |
[cleanup] Unify all calls to the error function.
This is the continuation of #244, we now deprecate `CErrors.error`,
the single entry point in Coq is `user_err`.
The rationale is to allow for easier grepping, and to ease a future
cleanup of error messages. In particular, we would like to
systematically classify all error messages raised by Coq and be sure
they are properly documented.
We restore the two functions removed in #244 to improve compatibility,
but mark them deprecated.
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4ada91eb5..98e71c7fd 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1050,7 +1050,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates = | None -> None,candidates | Some filter -> restrict_hyps evd evk filter candidates in match candidates,filter with - | UpdateWith [], _ -> error "Not solvable." + | UpdateWith [], _ -> user_err Pp.(str "Not solvable.") | UpdateWith [nc],_ -> let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in raise (EvarSolvedWhileRestricting (evd,mkEvar ev)) @@ -1230,7 +1230,7 @@ let check_evar_instance evd evk1 body conv_algo = (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) let ty = try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> error "Ill-typed evar instance" + with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") in match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with | Success evd -> evd |