diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 39 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 19 |
3 files changed, 38 insertions, 22 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index f7d78551d8..a0627dbe63 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -581,7 +581,7 @@ let rec locate_ref = function with Nametab.GlobalizationError _ | UserError _ -> None in match mpo, ro with - | None, None -> Nametab.error_global_not_found qid + | None, None -> Nametab.error_global_not_found ~info:Exninfo.null qid | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 53dc518bd3..bcfdb5318e 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -97,13 +97,19 @@ let intern_global_reference ist qid = else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then let id = qualid_basename qid in ArgArg (qid.CAst.loc, GlobRef.VarRef id) - else match locate_global_with_alias ~head:true qid with - | r -> ArgArg (qid.CAst.loc, r) - | exception Not_found -> - if not !strict_check && qualid_is_ident qid then - let id = qualid_basename qid in - ArgArg (qid.CAst.loc, GlobRef.VarRef id) - else Nametab.error_global_not_found qid + else + let r = + try locate_global_with_alias ~head:true qid + with + | Not_found as exn -> + if not !strict_check && qualid_is_ident qid then + let id = qualid_basename qid in + GlobRef.VarRef id + else + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid + in + ArgArg (qid.CAst.loc, r) let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -148,9 +154,10 @@ let intern_isolated_tactic_reference strict ist qid = with Not_found -> (* Tolerance for compatibility, allow not to use "constr:" *) try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) - with Not_found -> - (* Reference not found *) - Nametab.error_global_not_found qid + with Not_found as exn -> + (* Reference not found *) + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid (* Internalize an applied tactic reference *) @@ -167,9 +174,10 @@ let intern_applied_tactic_reference ist qid = with Not_found -> (* A global tactic *) try intern_applied_global_tactic_reference qid - with Not_found -> - (* Reference not found *) - Nametab.error_global_not_found qid + with Not_found as exn -> + (* Reference not found *) + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid (* Intern a reference parsed in a non-tactic entry *) @@ -182,7 +190,7 @@ let intern_non_tactic_reference strict ist qid = with Not_found -> (* Tolerance for compatibility, allow not to use "ltac:" *) try intern_isolated_global_tactic_reference qid - with Not_found -> + with Not_found as exn -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) if qualid_is_ident qid && not strict then let id = qualid_basename qid in @@ -190,7 +198,8 @@ let intern_non_tactic_reference strict ist qid = TacGeneric ipat else (* Reference not found *) - Nametab.error_global_not_found qid + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 6d350ade8d..5e8babbf80 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -378,7 +378,9 @@ let interp_reference ist env sigma = function with Not_found -> try GlobRef.VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) + with Not_found as exn -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -391,17 +393,21 @@ let interp_evaluable ist env sigma = function (* Maybe [id] has been introduced by Intro-like tactics *) begin try try_interp_evaluable env (loc, id) - with Not_found -> + with Not_found as exn -> match r with | EvalConstRef _ -> r - | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id) + | _ -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) + with Not_found as exn -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -663,8 +669,9 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let c = coerce_to_closed_constr env x in Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) - with Not_found -> - Nametab.error_global_not_found (qualid_of_ident ?loc id)) + with Not_found as exn -> + let _, info = Exninfo.capture exn in + Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p |