diff options
| author | delahaye | 2000-10-30 16:58:32 +0000 |
|---|---|---|
| committer | delahaye | 2000-10-30 16:58:32 +0000 |
| commit | db2be6c46d3882cadea3a14311d3ce7e21c53b83 (patch) | |
| tree | 538f7ef59ca0f0cf24f600b136c1179d02079f90 | |
| parent | 733e8bfbf80c1b6466c555410f83b8730151ba32 (diff) | |
Ajout d'un switch pour le debugger
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@790 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/vernacentries.ml | 16 | ||||
| -rw-r--r-- | toplevel/vernacinterp.ml | 2 |
2 files changed, 16 insertions, 2 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index afe871641e..8d109ab7ed 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -27,6 +27,8 @@ open Ast open Astterm open Pretty open Printer +open Tacinterp +open Tactic_debug open Command (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *) @@ -664,6 +666,18 @@ let _ = | _ -> bad_vernac_args "EndSilent") let _ = + add "DebugOn" + (function + | [] -> (fun () -> set_debug DebugOn) + | _ -> bad_vernac_args "DebugOn") + +let _ = + add "DebugOff" + (function + | [] -> (fun () -> set_debug DebugOff) + | _ -> bad_vernac_args "DebugOff") + +let _ = add "StartProof" (function | [VARG_STRING kind;VARG_IDENTIFIER s;VARG_CONSTR com] -> @@ -1205,7 +1219,7 @@ let _ = (let rec tacdef_fun lacc=function (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl -> let ve= - Tacinterp.val_interp (empty,empty_env,[],[],None) tacexp + val_interp (empty,empty_env,[],[],None,get_debug ()) tacexp in tacdef_fun ((string_of_id name,ve)::lacc) tl |[] -> diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 5308efba17..602818ccd0 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -97,7 +97,7 @@ let rec cvt_varg ast = | Node(_,"ASTLIST",al) -> VARG_ASTLIST al | Node(_,"TACTIC_ARG",[targ]) -> let (evc,env)= Command.get_current_context () in - VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None) targ) + VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None,get_debug ()) targ) | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg", [< 'sTR "Unrecognizable ast node of vernac arg:"; |