diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-18 16:57:48 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-18 16:57:48 +0000 |
| commit | 30302a47d06b3d92238524e7727b380f90960d40 (patch) | |
| tree | f37d572d42c20a97dd603ca33d0df995b3406a1b /toplevel | |
| parent | 4a3c8ae008d0159e4626497e94fd820489a2cf54 (diff) | |
Updating the backtrace handling mechanism to accomodate the new
exception information addition facility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16213 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 3 | ||||
| -rw-r--r-- | toplevel/mltop.ml | 2 |
2 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 525a924ed..51e567f0a 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -12,8 +12,7 @@ open Pp let (/) = Filename.concat let set_debug () = - let () = Printexc.record_backtrace true in - let () = Errors.record_backtrace () in + let () = Backtrace.record_backtrace true in Flags.debug := true (* Loading of the ressource file. diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index d5d8b1076..59fb3bbc1 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -121,7 +121,7 @@ let dir_ml_load s = let e = Errors.push e in match e with | (UserError _ | Failure _ | Not_found as u) -> raise u - | u when is_anomaly u -> reraise u + | u when is_anomaly u -> raise u | exc -> let msg = report_on_load_obj_error exc in errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++ |