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/reductionops.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/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 117ed338e..e7c963582 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1219,7 +1219,7 @@ let clos_norm_flags flgs env sigma t = EConstr.of_constr (CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let clos_whd_flags flgs env sigma t = try @@ -1227,7 +1227,7 @@ let clos_whd_flags flgs env sigma t = EConstr.of_constr (CClosure.whd_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) |