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 /kernel/inductive.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 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d8d365c34..4f4b641b4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -25,7 +25,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body let lookup_mind_specif env (kn,tyi) = let mib = Environ.lookup_mind kn env in if tyi >= Array.length mib.mind_packets then - error "Inductive.lookup_mind_specif: invalid inductive index"; + user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index"); (mib, mib.mind_packets.(tyi)) let find_rectype env c = @@ -247,7 +247,7 @@ let type_of_constructor (cstr, u) (mib,mip) = let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type."; + if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = |