Capture exception info

Author: yannl35133

proofs/clenv.ml

@@ -436,19 +436,21 @@ let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
     let metas = clenv.metam in
     let metas, sigma = w_unify ~metas ~flags clenv.env clenv.evd cv_pb t1 t2 in
     update_clenv_evd clenv sigma metas
-  with Pretype_errors.(PretypeError (env, sigma, CannotUnify (t1, t2, reason))) ->
+  with Pretype_errors.(PretypeError (env, sigma, CannotUnify (t1, t2, reason))) as exn ->
+    let _, info = Exninfo.capture exn in
     let sigma, f = replace_clenv_metas env sigma clenv in
-    raise (Pretype_errors.(PretypeError (env, sigma, CannotUnify (f t1, f t2, reason))))
+    Exninfo.iraise (Pretype_errors.(PretypeError (env, sigma, CannotUnify (f t1, f t2, reason))), info)
 
 
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   try
     let metas = clenv.metam in
     let metas, sigma = w_unify_meta_types ~metas ~flags:flags clenv.env clenv.evd in
     update_clenv_evd clenv sigma metas
-  with Pretype_errors.(PretypeError (env, sigma, CannotUnify (t1, t2, reason))) ->
+  with Pretype_errors.(PretypeError (env, sigma, CannotUnify (t1, t2, reason))) as exn ->
+    let _, info = Exninfo.capture exn in
     let sigma, f = replace_clenv_metas env sigma clenv in
-    raise (Pretype_errors.(PretypeError (env, sigma, CannotUnify (f t1, f t2, reason))))
+    Exninfo.iraise (Pretype_errors.(PretypeError (env, sigma, CannotUnify (f t1, f t2, reason))), info)
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv concl =
   let metas = meta_handler clenv.metam in