diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-21 10:19:59 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-21 10:19:59 +0000 |
commit | f070d33f9822dac079e58a9920c9c9e0cade12f6 (patch) | |
tree | 9ddea6b144ca133d323d7ec2e6659a0bb3a650f8 /contrib/correctness | |
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')
-rw-r--r-- | contrib/correctness/pmisc.ml | 6 | ||||
-rw-r--r-- | contrib/correctness/pmisc.mli | 1 | ||||
-rw-r--r-- | contrib/correctness/psyntax.ml4 | 10 |
3 files changed, 2 insertions, 15 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 diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli index e93f20a61..9e32f147e 100644 --- a/contrib/correctness/pmisc.mli +++ b/contrib/correctness/pmisc.mli @@ -70,7 +70,6 @@ val abstract : (identifier * constr) list -> constr -> constr (* for debugging purposes *) -val debug : bool ref val deb_mess : Pp.std_ppcmds -> unit val deb_print : ('a -> Pp.std_ppcmds) -> 'a -> unit diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index e1fd72fb4..0791dab78 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -499,12 +499,6 @@ let is_assumed global ids = let add = vinterp_add -let _ = add "PROGDEBUGON" - (function [] -> fun () -> debug := true | _ -> assert false) - -let _ = add "PROGDEBUGOFF" - (function [] -> fun () -> debug := false | _ -> assert false) - let _ = add "CORRECTNESS" (function [ VARG_STRING s; VARG_DYN d ] -> @@ -583,10 +577,6 @@ GEXTEND Gram let d = Ast.dynamic (in_prog p) in let str = Ast.string s in <:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >> ] ]; - Pcoq.Vernac_.command: - [ [ IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >> - - | IDENT "Debug"; IDENT "off"; "." -> <:ast< (PROGDEBUGOFF) >> ] ]; END ;; |