aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml15
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_tactic.ml46
-rw-r--r--plugins/ltac/pptactic.ml8
-rw-r--r--plugins/ltac/rewrite.ml12
-rw-r--r--plugins/ltac/tacentries.ml12
-rw-r--r--plugins/ltac/tacintern.ml2
8 files changed, 29 insertions, 30 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 470a93f2b..bf84f61a5 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -56,17 +56,16 @@ let instantiate_tac n c ido =
InHyp ->
(match decl with
| LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ)
- | _ -> error
- "Please be more specific: in type or value?")
+ | _ -> user_err Pp.(str "Please be more specific: in type or value?"))
| InHypTypeOnly ->
evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
| InHypValueOnly ->
(match decl with
| LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
- | _ -> error "Not a defined hypothesis.") in
+ | _ -> user_err Pp.(str "Not a defined hypothesis.")) in
if List.length evl < n then
- error "Not enough uninstantiated existential variables.";
- if n <= 0 then error "Incorrect existential variable index.";
+ user_err Pp.(str "Not enough uninstantiated existential variables.");
+ if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let evk,_ = List.nth evl (n-1) in
instantiate_evar evk c sigma gl
end
@@ -76,7 +75,7 @@ let instantiate_tac_by_name id c =
let sigma = gl.sigma in
let evk =
try Evd.evar_key id sigma
- with Not_found -> error "Unknown existential variable." in
+ with Not_found -> user_err Pp.(str "Unknown existential variable.") in
instantiate_evar evk c sigma gl
end
@@ -109,8 +108,8 @@ let hget_evar n =
let concl = Proofview.Goal.concl gl in
let evl = evar_list sigma concl in
if List.length evl < n then
- error "Not enough uninstantiated existential variables.";
- if n <= 0 then error "Incorrect existential variable index.";
+ user_err Pp.(str "Not enough uninstantiated existential variables.");
+ if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let ev = List.nth evl (n-1) in
let ev_type = EConstr.existential_type sigma ev in
Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index a3310c2d8..fdb8d3461 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -90,7 +90,7 @@ let occurrences_of = function
| n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl)
| nl ->
if List.exists (fun n -> n < 0) nl then
- CErrors.error "Illegal negative occurrence number.";
+ CErrors.user_err Pp.(str "Illegal negative occurrence number.");
OnlyOccurrences nl
let coerce_to_int v = match Value.to_int v with
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 5273eb3b5..d68139a4b 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1085,7 +1085,7 @@ let decompose l c =
let sigma = Tacmach.New.project gl in
let to_ind c =
if isInd sigma c then fst (destInd sigma c)
- else error "not an inductive type"
+ else user_err Pp.(str "not an inductive type")
in
let l = List.map to_ind l in
Elim.h_decompose l c
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 257100b01..1404b1c1f 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -117,8 +117,8 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
| _, Some x ->
let ids = List.map snd (List.flatten (List.map pi1 bl)) in
(try List.index Names.Name.equal (snd x) ids
- with Not_found -> error "No such fix variable.")
- | _ -> error "Cannot guess decreasing argument of fix." in
+ with Not_found -> user_err Pp.(str "No such fix variable."))
+ | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in
(id,n, CAst.make ~loc @@ CProdN(bl,ty))
let mk_cofix_tac (loc,id,bl,ann,ty) =
@@ -152,7 +152,7 @@ let mkTacCase with_evar = function
| ic ->
if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
then
- error "Use of numbers as direct arguments of 'case' is not supported.";
+ user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported.");
TacInductionDestruct (false,with_evar,ic)
let rec mkCLambdaN_simple_loc ?loc bll c =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 75ab1c5ee..a001c6a2b 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -348,7 +348,7 @@ type 'a extra_genarg_printer =
let bll = List.map (fun (x, _, y) -> x, y) bll in
if nb >= n then (List.rev (bll@acc)), a
else strip_ty (bll@acc) (n-nb) a
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_ltac_or_var pr = function
@@ -1089,7 +1089,7 @@ type 'a extra_genarg_printer =
match ty.CAst.v with
Glob_term.GProd(na,Explicit,a,b) ->
strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let raw_printers =
@@ -1160,7 +1160,7 @@ type 'a extra_genarg_printer =
match Term.kind_of_term ty with
Term.Prod(na,a,b) ->
strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_atomic_tactic_level env sigma n t =
@@ -1210,7 +1210,7 @@ let declare_extra_genarg_pprule wit
(h : 'c extra_genarg_printer) =
begin match wit with
| ExtraArg s -> ()
- | _ -> error "Can declare a pretty-printing rule only for extra argument types."
+ | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
end;
let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
let g x =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b0db2839b..966b11d0e 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -235,7 +235,7 @@ end) = struct
let liftarg = mkLambda (na, ty, arg) in
let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
- else error "build_signature: no constraint can apply on a dependent argument"
+ else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
| _, [] ->
(match finalcstr with
@@ -472,7 +472,7 @@ type hypinfo = {
let get_symmetric_proof b =
if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
-let error_no_relation () = error "Cannot find a relation to rewrite."
+let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
let rec decompose_app_rel env evd t =
(** Head normalize for compatibility with the old meta mechanism *)
@@ -525,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) =
let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
| Some c -> c
- | None -> error "Cannot find an homogeneous relation to rewrite."
+ | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")
let rewrite_db = "rewrite"
@@ -831,7 +831,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
sigargs, r.rew_to :: typeargs')
| None ->
if not (Option.is_empty y) then
- error "Cannot rewrite inside dependent arguments of a function";
+ user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
x :: acc, x :: subst, evars, sigargs, x :: typeargs')
([], [], evars, sigargs, []) args args'
in
@@ -1419,7 +1419,7 @@ module Strategies =
let unfolded =
try Tacred.try_red_product env sigma c
with e when CErrors.noncritical e ->
- error "fold: the term is not unfoldable !"
+ user_err Pp.(str "fold: the term is not unfoldable !")
in
try
let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
@@ -2198,7 +2198,7 @@ let setoid_symmetry_in id =
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z -> let l,res = split_last_two (y::z) in x::l, res
- | _ -> error "Cannot find an equivalence relation to rewrite."
+ | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.")
in
let others,(c1,c2) = split_last_two args in
let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4d7b0f929..75f89a81e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -60,7 +60,7 @@ let get_tacentry n m =
else EntryName (rawwit Tacarg.wit_tactic, atactic n)
let get_separator = function
-| None -> error "Missing separator."
+| None -> user_err Pp.(str "Missing separator.")
| Some sep -> sep
let rec parse_user_entry s sep =
@@ -110,7 +110,7 @@ let get_tactic_entry n =
else if 1<=n && n<5 then
Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
else
- error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+ user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
(**********************************************************************)
(** State of the grammar extensions *)
@@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state =
in
let () =
if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
- error "Notation for simple tactic must start with an identifier."
+ user_err Pp.(str "Notation for simple tactic must start with an identifier.")
in
let map = function
| TacTerm s -> GramTerminal s
@@ -208,7 +208,7 @@ let interp_prod_item = function
| None ->
if String.Map.mem s !entry_names then String.Map.find s !entry_names
else begin match ArgT.name s with
- | None -> error ("Unknown entry "^s^".")
+ | None -> user_err Pp.(str ("Unknown entry "^s^"."))
| Some arg -> arg
end
| Some n ->
@@ -253,8 +253,8 @@ let pprule pa = {
let check_key key =
if Tacenv.check_alias key then
- error "Conflicting tactic notations keys. This can happen when including \
- twice the same module."
+ user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \
+ twice the same module.")
let cache_tactic_notation (_, tobj) =
let key = tobj.tacobj_key in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 6c7eb8c89..e431a13bc 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -252,7 +252,7 @@ and intern_or_and_intro_pattern lf ist = function
let intern_or_and_intro_pattern_loc lf ist = function
| ArgVar (_,id) as x ->
if find_var id ist then x
- else error "Disjunctive/conjunctive introduction pattern expected."
+ else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.")
| ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
let intern_intro_pattern_naming_loc lf ist (loc,pat) =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 20:45:39 +0000