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 /plugins/funind/recdef.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 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c46309355..e206955ac 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -136,7 +136,7 @@ let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" - with Not_found -> error "module Recdef not loaded" + with Not_found -> user_err Pp.(str "module Recdef not loaded") let iter = function () -> (constr_of_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") @@ -323,8 +323,8 @@ let check_not_nested sigma forbidden e = | Construct _ -> () | Case(_,t,e,a) -> check_not_nested t;check_not_nested e;Array.iter check_not_nested a - | Fix _ -> error "check_not_nested : Fix" - | CoFix _ -> error "check_not_nested : Fix" + | Fix _ -> user_err Pp.(str "check_not_nested : Fix") + | CoFix _ -> user_err Pp.(str "check_not_nested : Fix") in try check_not_nested e @@ -430,8 +430,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = let sigma = project g in match EConstr.kind sigma expr_info.info with - | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint" - | Proj _ -> error "Function cannot treat projections" + | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") + | Proj _ -> user_err Pp.(str "Function cannot treat projections") | LetIn(na,b,t,e) -> begin let new_continuation_tac = @@ -1304,7 +1304,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp in let na = next_global_ident_away name [] in if Termops.occur_existential sigma gls_type then - CErrors.error "\"abstract\" cannot handle existentials"; + CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = let na_ref = Libnames.Ident (Loc.tag na) in |