diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pputils.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 4 | ||||
| -rw-r--r-- | printing/printer.ml | 6 |
3 files changed, 6 insertions, 6 deletions
diff --git a/printing/pputils.ml b/printing/pputils.ml index d1ba1a4a10..99d07601c4 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -96,7 +96,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l) | Red true -> - CErrors.error "Shouldn't be accessible from user." + CErrors.user_err Pp.(str "Shouldn't be accessible from user.") | ExtraRedExpr s -> str s | CbvVm o -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 70de65acdc..0f7da36133 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -716,7 +716,7 @@ let read_sec_context r = | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | (_,Lib.ClosedSection _)::rest -> - error "Cannot print the contents of a closed section." + user_err Pp.(str "Cannot print the contents of a closed section.") (* LEM: Actually, we could if we wanted to. *) | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest @@ -765,7 +765,7 @@ let print_opaque_name qid = if Declareops.constant_has_body cb then print_constant_with_infos cst else - error "Not a defined constant." + user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> diff --git a/printing/printer.ml b/printing/printer.ml index d4f7afb38c..ebe68680fb 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -566,7 +566,7 @@ let pr_selected_subgoal name sigma g = let default_pr_subgoal n sigma = let rec prrec p = function - | [] -> error "No such goal." + | [] -> user_err Pp.(str "No such goal.") | g::rest -> if Int.equal p 1 then pr_selected_subgoal (int n) sigma g @@ -828,7 +828,7 @@ let pr_goal_by_id id = Proof.in_proof p (fun sigma -> let g = Evd.evar_key id sigma in pr_selected_subgoal (pr_id id) sigma g) - with Not_found -> error "No such goal." + with Not_found -> user_err Pp.(str "No such goal.") let pr_goal_by_uid uid = let p = Proof_global.give_me_the_proof () in @@ -839,7 +839,7 @@ let pr_goal_by_uid uid = in try Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;}) - with Not_found -> error "Invalid goal identifier." + with Not_found -> user_err Pp.(str "Invalid goal identifier.") (* Elementary tactics *) |