diff options
| -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:"; |