aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/evar_refiner.ml4
-rw-r--r--proofs/logic.ml2
-rw-r--r--proofs/pfedit.ml10
-rw-r--r--proofs/proof.ml16
-rw-r--r--proofs/proof_global.ml14
6 files changed, 25 insertions, 25 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 9e0a2a03eb..33a86402ef 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -163,7 +163,7 @@ let error_incompatible_inst clenv mv =
let clenv_assign mv rhs clenv =
let rhs_fls = mk_freelisted rhs in
if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then
- error "clenv_assign: circularity in unification";
+ user_err Pp.(str "clenv_assign: circularity in unification");
try
if meta_defined clenv.evd mv then
if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
@@ -174,7 +174,7 @@ let clenv_assign mv rhs clenv =
let st = (Conv,TypeNotProcessed) in
{clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
with Not_found ->
- error "clenv_assign: undefined meta"
+ user_err Pp.(str "clenv_assign: undefined meta")
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b9c9257969..b1fe128a24 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -39,11 +39,11 @@ let define_and_solve_constraints evk c env evd =
pbs
with
| Success evd -> evd
- | UnifFailure _ -> error "Instance does not satisfy the constraints."
+ | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.")
let w_refine (evk,evi) (ltac_var,rawc) sigma =
if Evd.is_defined sigma evk then
- error "Instantiate called on already-defined evar";
+ user_err Pp.(str "Instantiate called on already-defined evar");
let env = Evd.evar_filtered_env evi in
let sigma',typed_c =
let flags = {
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 54345abd97..cd2cfbd32f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -141,7 +141,7 @@ let occur_vars_in_decl env sigma hyps d =
let reorder_context env sigma sign ord =
let ords = List.fold_right Id.Set.add ord Id.Set.empty in
if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
- error "Order list has duplicates";
+ user_err Pp.(str "Order list has duplicates");
let rec step ord expected ctxt_head moved_hyps ctxt_tail =
match ord with
| [] -> List.rev ctxt_tail @ ctxt_head
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 92b4e788a2..aaceb7b762 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -71,7 +71,7 @@ let get_universe_binders () =
exception NoSuchGoal
let _ = CErrors.register_handler begin function
- | NoSuchGoal -> CErrors.error "No such goal."
+ | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
| _ -> raise CErrors.Unhandled
end
let get_nth_V82_goal i =
@@ -87,12 +87,12 @@ let get_goal_context_gen i =
let get_goal_context i =
try get_goal_context_gen i
- with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
- | NoSuchGoal -> CErrors.error "No such goal."
+ with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
+ | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
let get_current_goal_context () =
try get_goal_context_gen 1
- with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+ with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
| NoSuchGoal ->
(* spiwack: returning empty evar_map, since if there is no goal, under focus,
there is no accessible evar either *)
@@ -143,7 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
in
(p,status)
with
- Proof_global.NoCurrentProof -> CErrors.error "No focused proof"
+ Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index b2103489a7..2aa620c1da 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -66,14 +66,14 @@ exception FullyUnfocused
let _ = CErrors.register_handler begin function
| CannotUnfocusThisWay ->
- CErrors.error "This proof is focused, but cannot be unfocused this way"
+ CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way")
| NoSuchGoals (i,j) when Int.equal i j ->
CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
| NoSuchGoals (i,j) ->
CErrors.user_err ~hdr:"Focus" Pp.(
str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
)
- | FullyUnfocused -> CErrors.error "The proof is not focused"
+ | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
| _ -> raise CErrors.Unhandled
end
@@ -301,10 +301,10 @@ exception HasShelvedGoals
exception HasGivenUpGoals
exception HasUnresolvedEvar
let _ = CErrors.register_handler begin function
- | UnfinishedProof -> CErrors.error "Some goals have not been solved."
- | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
- | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
- | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+ | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.")
+ | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.")
+ | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.")
+ | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.")
| _ -> raise CErrors.Unhandled
end
@@ -420,9 +420,9 @@ module V82 = struct
let evl = Evarutil.non_instantiated sigma in
let evl = Evar.Map.bindings evl in
if (n <= 0) then
- CErrors.error "incorrect existential variable index"
+ CErrors.user_err Pp.(str "incorrect existential variable index")
else if CList.length evl < n then
- CErrors.error "not so many uninstantiated existential variables"
+ CErrors.user_err Pp.(str "not so many uninstantiated existential variables")
else
CList.nth evl (n-1)
in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 95aee72cb5..4d2f534a76 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,7 +36,7 @@ let proof_modes = Hashtbl.create 6
let find_proof_mode n =
try Hashtbl.find proof_modes n
with Not_found ->
- CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
+ CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n))
let register_proof_mode ({name = n} as m) =
Hashtbl.add proof_modes n (CEphemeron.create m)
@@ -124,13 +124,13 @@ let push a l = l := a::!l;
exception NoSuchProof
let _ = CErrors.register_handler begin function
- | NoSuchProof -> CErrors.error "No such proof."
+ | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.")
| _ -> raise CErrors.Unhandled
end
exception NoCurrentProof
let _ = CErrors.register_handler begin function
- | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+ | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
| _ -> raise CErrors.Unhandled
end
@@ -299,7 +299,7 @@ let set_used_variables l =
| [] -> raise NoCurrentProof
| p :: rest ->
if not (Option.is_empty p.section_vars) then
- CErrors.error "Used section variables can be declared only once";
+ CErrors.user_err Pp.(str "Used section variables can be declared only once");
pstates := { p with section_vars = Some ctx} :: rest;
ctx, to_clear
@@ -637,7 +637,7 @@ module Bullet = struct
current_behavior :=
try Hashtbl.find behaviors n
with Not_found ->
- CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
+ CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
end
})
@@ -687,9 +687,9 @@ let parse_goal_selector = function
let err_msg = "The default selector must be \"all\" or a natural number." in
begin try
let i = int_of_string i in
- if i < 0 then CErrors.error err_msg;
+ if i < 0 then CErrors.user_err Pp.(str err_msg);
Vernacexpr.SelectNth i
- with Failure _ -> CErrors.error err_msg
+ with Failure _ -> CErrors.user_err Pp.(str err_msg)
end
let _ =
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 21:13:46 +0000