diff options
author | 2002-02-21 10:19:59 +0000 | |
---|---|---|
committer | 2002-02-21 10:19:59 +0000 | |
commit | f070d33f9822dac079e58a9920c9c9e0cade12f6 (patch) | |
tree | 9ddea6b144ca133d323d7ec2e6659a0bb3a650f8 /contrib/correctness/pmisc.ml | |
parent | b7aa648034f73c390ba2b49c8d47c3c8277002ef (diff) |
code mort dans tactinterp; plus de Debug On/Off dans Correctness
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2490 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/pmisc.ml')
-rw-r--r-- | contrib/correctness/pmisc.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml index 6d0ad0fb0..bb9f539bb 100644 --- a/contrib/correctness/pmisc.ml +++ b/contrib/correctness/pmisc.ml @@ -18,15 +18,13 @@ open Term (* debug *) -let debug = ref false - let deb_mess s = - if !debug then begin + if !Options.debug then begin msgnl s; pp_flush() end let deb_print f x = - if !debug then begin + if !Options.debug then begin msgnl (f x); pp_flush() end |