aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authordelahaye2003-02-13 13:01:22 +0000
committerdelahaye2003-02-13 13:01:22 +0000
commit75f4910db440eb081a22cafccf01e1dbcb12b8c4 (patch)
treef9330eb3981ead6f7d3e567ce552e61cce021afb /toplevel
parent0b241e3ae3215f4aa9c4c98973ec366a33273d5b (diff)
Debugger plus informatif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3675 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/cerrors.ml2
-rw-r--r--toplevel/vernacentries.ml2
2 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 129794c587..45fe9995ef 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -115,6 +115,8 @@ let rec explain_exn_default = function
let raise_if_debug e =
if !Options.debug then raise e
+let _ = Tactic_debug.explain_logic_error := explain_exn_default
+
let explain_exn_function = ref explain_exn_default
let explain_exn e = !explain_exn_function e
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6a282d5477..ef5430e3b9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1036,7 +1036,7 @@ let vernac_check_guard () =
msgnl message
let vernac_debug b =
- set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
+ set_debug (if b then Tactic_debug.DebugOn else Tactic_debug.DebugOff)
(**************************)