[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...

1 files changed, 6 insertions, 4 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 6994a7b78f..414663c826 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -69,15 +69,17 @@ let precatchable_exception = function
   | Nametab.GlobalizationError _ -> true
   | _ -> false
 
-let raise_pretype_error ?loc (env,sigma,te) =
-  Loc.raise ?loc (PretypeError(env,sigma,te))
+let raise_pretype_error ?loc ?info (env,sigma,te) =
+  let info = Option.default Exninfo.null info in
+  let info = Option.cata (Loc.add_loc info) info loc in
+  Exninfo.iraise (PretypeError(env,sigma,te),info)
 
 let raise_type_error ?loc (env,sigma,te) =
   Loc.raise ?loc (PretypeError(env,sigma,TypingError te))
 
-let error_actual_type ?loc env sigma {uj_val=c;uj_type=actty} expty reason =
+let error_actual_type ?loc ?info env sigma {uj_val=c;uj_type=actty} expty reason =
   let j = {uj_val=c;uj_type=actty} in
-  raise_pretype_error ?loc
+  raise_pretype_error ?loc ?info
     (env, sigma, ActualTypeNotCoercible (j, expty, reason))
 
 let error_actual_type_core ?loc env sigma {uj_val=c;uj_type=actty} expty =