aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/g_ltac.ml42
-rw-r--r--ltac/rewrite.ml4
-rw-r--r--ltac/tacentries.ml4
-rw-r--r--ltac/tacenv.ml2
-rw-r--r--ltac/tacintern.ml6
-rw-r--r--ltac/tacinterp.ml18
6 files changed, 18 insertions, 18 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 85f1a0225..c67af33e2 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -36,7 +36,7 @@ let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
let reference_to_id = function
| Libnames.Ident (loc, id) -> (loc, id)
| Libnames.Qualid (loc,_) ->
- CErrors.user_err ~loc ""
+ CErrors.user_err ~loc
(str "This expression should be a simple identifier.")
let tactic_mode = Gram.entry_create "vernac:tactic_command"
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index e0583370a..18f67cad4 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1508,7 +1508,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
Evar.Set.fold
(fun ev acc ->
if not (Evd.is_defined acc ev) then
- user_err "rewrite"
+ user_err ~hdr:"rewrite"
(str "Unsolved constraint remaining: " ++ spc () ++
Evd.pr_evar_info (Evd.find acc ev))
else Evd.remove acc ev)
@@ -1647,7 +1647,7 @@ let cl_rewrite_clause_strat progress strat clause =
(fun gl ->
try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl
with RewriteFailure e ->
- user_err "" (str"setoid rewrite failed: " ++ e)
+ user_err (str"setoid rewrite failed: " ++ e)
| Refiner.FailError (n, pp) ->
tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl))
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 1b7430c3f..2fed0e14f 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -429,7 +429,7 @@ let register_ltac local tacl =
let kn = Lib.make_kn id in
let id_pp = pr_id id in
let () = if is_defined_tac kn then
- CErrors.user_err ~loc ""
+ CErrors.user_err ~loc
(str "There is already an Ltac named " ++ id_pp ++ str".")
in
let is_shadowed =
@@ -446,7 +446,7 @@ let register_ltac local tacl =
let kn =
try Nametab.locate_tactic (snd (qualid_of_reference ident))
with Not_found ->
- CErrors.user_err ~loc ""
+ CErrors.user_err ~loc
(str "There is no Ltac named " ++ pr_reference ident ++ str ".")
in
UpdateTac kn, body
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index 5808feeba..e3c2b4ad5 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
let () = if Array.length tacs <= i then raise Not_found in
tacs.(i)
with Not_found ->
- CErrors.user_err ""
+ CErrors.user_err
(str "The tactic " ++ pr_tacname s ++ str " is not installed.")
(***************************************************************************)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index a1d34b53f..cd791398d 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -33,7 +33,7 @@ open Locus
let dloc = Loc.ghost
let error_tactic_expected ?loc =
- user_err ?loc "" (str "Tactic expected.")
+ user_err ?loc (str "Tactic expected.")
(** Generic arguments *)
@@ -461,7 +461,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
let extract_let_names lrc =
let fold accu ((loc, name), _) =
if Id.Set.mem name accu then user_err ~loc
- "glob_tactic" (str "This variable is bound several times.")
+ ~hdr:"glob_tactic" (str "This variable is bound several times.")
else Id.Set.add name accu
in
List.fold_left fold Id.Set.empty lrc
@@ -748,7 +748,7 @@ let print_ltac id =
++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
with
Not_found ->
- user_err "print_ltac"
+ user_err ~hdr:"print_ltac"
(pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
(** Registering *)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index b1f554eaa..7d447b236 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -168,7 +168,7 @@ module Value = struct
let pr_v = Pptactic.pr_value Pptactic.ltop v in
let Val.Dyn (tag, _) = v in
let tag = Val.pr tag in
- user_err "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
+ user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
++ str " while type " ++ Val.pr wit ++ str " was expected.")
let unbox wit v ans = match ans with
@@ -315,7 +315,7 @@ let append_trace trace v =
(* Dynamically check that an argument is a tactic *)
let coerce_to_tactic loc id v =
let v = Value.normalize v in
- let fail () = user_err ~loc ""
+ let fail () = user_err ~loc
(str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
in
let v = Value.normalize v in
@@ -371,7 +371,7 @@ let debugging_exception_step ist signal_anomaly e pp =
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
let error_ltac_variable loc id env v s =
- user_err ~loc "" (str "Ltac variable " ++ pr_id id ++
+ user_err ~loc (str "Ltac variable " ++ pr_id id ++
strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
strbrk "which cannot be coerced to " ++ str s ++ str".")
@@ -404,7 +404,7 @@ let interp_intro_pattern_naming_var loc ist env sigma id =
let interp_int ist locid =
try try_interp_ltac_var coerce_to_int ist None locid
with Not_found ->
- user_err ~loc:(fst locid) "interp_int"
+ user_err ~loc:(fst locid) ~hdr:"interp_int"
(str "Unbound variable " ++ pr_id (snd locid) ++ str".")
let interp_int_or_var ist = function
@@ -795,7 +795,7 @@ let interp_may_eval f ist env sigma = function
!evdref , c
with
| Not_found ->
- user_err ~loc "interp_may_eval"
+ user_err ~loc ~hdr:"interp_may_eval"
(str "Unbound context identifier" ++ pr_id s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
@@ -1032,7 +1032,7 @@ let interp_destruction_arg ist gl arg =
}
| keep,ElimOnAnonHyp n as x -> x
| keep,ElimOnIdent (loc,id) ->
- let error () = user_err ~loc ""
+ let error () = user_err ~loc
(strbrk "Cannot coerce " ++ pr_id id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
@@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg =
(keep, ElimOnConstr { delayed = begin fun env sigma ->
try Sigma.here (constr_of_id env id', NoBindings) sigma
with Not_found ->
- user_err ~loc "interp_destruction_arg" (
+ user_err ~loc ~hdr:"interp_destruction_arg" (
pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
end })
in
@@ -1111,7 +1111,7 @@ let read_pattern lfun ist env sigma = function
(* Reads the hypotheses of a Match Context rule *)
let cons_and_check_name id l =
if Id.List.mem id l then
- user_err "read_match_goal_hyps" (
+ user_err ~hdr:"read_match_goal_hyps" (
str "Hypothesis pattern-matching variable " ++ pr_id id ++
str " used twice in the same pattern.")
else id::l
@@ -1870,7 +1870,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let (sigma, c) = interp_constr ist env sigma c in
Sigma.Unsafe.of_pair (c, sigma)
with e when to_catch e (* Hack *) ->
- user_err "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+ user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
end } in
Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
end }
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 08:48:29 +0000