Preserve backtrace for retyping anomalies

Author: yannl35133

pretyping/retyping.ml

@@ -56,7 +56,9 @@ let retype_error re = raise (RetypeError re)
 
 let anomaly_on_error f x =
  try f x
- with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e ++ str ".")
+ with RetypeError e as exn ->
+  let _, info = Exninfo.capture exn in
+  anomaly ~label:"retyping" ~info (print_retype_error e ++ str ".")
 
 let get_type_from_constraints env sigma t =
   if isEvar sigma (fst (decompose_app sigma t)) then