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 /vernac/indschemes.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 'vernac/indschemes.ml')
| -rw-r--r-- | vernac/indschemes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index b21e80bef..a78221301 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -418,7 +418,7 @@ let get_common_underlying_mutual_inductive = function raise (RecursionSchemeError (NotMutualInScheme (ind,ind'))) | [] -> if not (List.distinct_f Int.compare (List.map snd (List.map snd all))) - then error "A type occurs twice"; + then user_err Pp.(str "A type occurs twice"); mind, List.map_filter (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all @@ -429,7 +429,7 @@ let do_scheme l = tried to declare different schemes at once *) if not (List.is_empty ischeme) && not (List.is_empty escheme) then - error "Do not declare equality and induction scheme at the same time." + user_err Pp.(str "Do not declare equality and induction scheme at the same time.") else ( if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme else @@ -497,7 +497,7 @@ let do_combined_scheme name schemes = let refe = Ident x in let qualid = qualid_of_reference refe in try Nametab.locate_constant (snd qualid) - with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared.")) + with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared.")) schemes in let body,typ = build_combined_scheme (Global.env ()) csts in |