diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-29 00:45:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-29 00:45:16 +0200 |
| commit | 4c1260299b707bd27765b0ab365092046b134a69 (patch) | |
| tree | 22331e8562bee137a5d2eea79c0d8e3d43cb94c1 /plugins/funind/recdef.ml | |
| parent | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (diff) | |
| parent | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (diff) | |
Merge PR#512: [cleanup] Unify all calls to the error function.
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 00020609e..2f9f70876 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -138,7 +138,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") @@ -325,8 +325,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 @@ -432,8 +432,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 = @@ -1306,7 +1306,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 |