[misc] Better preserve backtraces in several modules

Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.

I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.

There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...

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