diff options
Diffstat (limited to 'ltac/tacintern.ml')
| -rw-r--r-- | ltac/tacintern.ml | 27 |
1 files changed, 12 insertions, 15 deletions
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index c5bb0ed07..cd791398d 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -32,11 +32,8 @@ open Locus let dloc = Loc.ghost -let error_global_not_found_loc (loc,qid) = - error_global_not_found_loc loc qid - -let error_tactic_expected loc = - user_err_loc (loc,"",str "Tactic expected.") +let error_tactic_expected ?loc = + user_err ?loc (str "Tactic expected.") (** Generic arguments *) @@ -85,7 +82,7 @@ let intern_hyp ist (loc,id as locid) = else if find_ident id ist then (dloc,id) else - Pretype_errors.error_var_not_found_loc loc id + Pretype_errors.error_var_not_found ~loc id let intern_or_var f ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) @@ -99,7 +96,7 @@ let intern_global_reference ist = function | r -> let loc,_ as lqid = qualid_of_reference r in try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> error_global_not_found_loc lqid + with Not_found -> error_global_not_found (snd lqid) let intern_ltac_variable ist = function | Ident (loc,id) -> @@ -143,7 +140,7 @@ let intern_isolated_tactic_reference strict ist r = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) + error_global_not_found (snd (qualid_of_reference r)) (* Internalize an applied tactic reference *) @@ -159,7 +156,7 @@ let intern_applied_tactic_reference ist r = try intern_applied_global_tactic_reference r with Not_found -> (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) + error_global_not_found (snd (qualid_of_reference r)) (* Intern a reference parsed in a non-tactic entry *) @@ -180,7 +177,7 @@ let intern_non_tactic_reference strict ist r = TacGeneric ipat | _ -> (* Reference not found *) - error_global_not_found_loc (qualid_of_reference r) + error_global_not_found (snd (qualid_of_reference r)) let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -291,7 +288,7 @@ let intern_evaluable_global_reference ist r = with Not_found -> match r with | Ident (loc,id) when not !strict_check -> EvalVarRef id - | _ -> error_global_not_found_loc lqid + | _ -> error_global_not_found (snd lqid) let intern_evaluable_reference_or_by_notation ist = function | AN r -> intern_evaluable_global_reference ist r @@ -463,8 +460,8 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = let fold accu ((loc, name), _) = - if Id.Set.mem name accu then user_err_loc - (loc, "glob_tactic", str "This variable is bound several times.") + if Id.Set.mem name accu then user_err ~loc + ~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 @@ -641,7 +638,7 @@ and intern_tactic_as_arg loc onlytac ist a = | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a -> - if onlytac then error_tactic_expected loc else TacArg (loc,a) + if onlytac then error_tactic_expected ~loc else TacArg (loc,a) and intern_tactic_or_tacarg ist = intern_tactic false ist @@ -751,7 +748,7 @@ let print_ltac id = ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined with Not_found -> - errorlabstrm "print_ltac" + user_err ~hdr:"print_ltac" (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") (** Registering *) |