diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 21:25:20 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-06 21:28:09 +0100 |
commit | cdc91f02f98b4d857bfebe61d95b920787a8d0e5 (patch) | |
tree | eefe365468ee275445ce0a00395d602f7c1ab48f /tactics | |
parent | 6f49db55e525a57378ca5600476c870a98a59dae (diff) |
Putting Tactic_debug just below Tacinterp.
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/ftactic.ml | 2 | ||||
-rw-r--r-- | tactics/ftactic.mli | 5 | ||||
-rw-r--r-- | tactics/tacenv.ml | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
-rw-r--r-- | tactics/tactic_debug.ml | 6 | ||||
-rw-r--r-- | tactics/tactic_debug.mli | 2 | ||||
-rw-r--r-- | tactics/tactics.mllib | 2 |
7 files changed, 4 insertions, 17 deletions
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index 55463afd0..588709873 100644 --- a/tactics/ftactic.ml +++ b/tactics/ftactic.ml @@ -99,8 +99,6 @@ end module Ftac = Monad.Make(Self) module List = Ftac.List -let debug_prompt = Tactic_debug.debug_prompt - module Notations = struct let (>>=) = bind diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli index fd05a4469..19041f169 100644 --- a/tactics/ftactic.mli +++ b/tactics/ftactic.mli @@ -70,11 +70,6 @@ val (<*>) : unit t -> 'a t -> 'a t module List : Monad.ListS with type 'a t := 'a t -(** {5 Debug} *) - -val debug_prompt : - int -> Tacexpr.glob_tactic_expr -> (Tactic_debug.debug_info -> 'a t) -> 'a t - (** {5 Notations} *) module Notations : diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index cc87e197d..d2d3f3117 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -143,5 +143,3 @@ let register_ltac for_ml local id tac = let redefine_ltac local kn tac = Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac)) - -let () = Hook.set Tactic_debug.is_ltac_for_ml_tactic_hook is_ltac_for_ml_tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 36a23d580..32f7c3c61 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1202,7 +1202,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti let ist = { ist with extra = TacStore.set ist.extra f_debug v } in value_interp ist >>= fun v -> return (name_vfun appl v) in - Ftactic.debug_prompt lev tac eval + Tactic_debug.debug_prompt lev tac eval | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml index fa40b7416..e991eb86d 100644 --- a/tactics/tactic_debug.ml +++ b/tactics/tactic_debug.ml @@ -325,12 +325,10 @@ let db_breakpoint debug s = (** Extrating traces *) -let (is_for_ml_f, is_ltac_for_ml_tactic_hook) = Hook.make () - let is_defined_ltac trace = let rec aux = function | (_, Tacexpr.LtacNameCall f) :: tail -> - not (Hook.get is_for_ml_f f) + not (Tacenv.is_ltac_for_ml_tactic f) | (_, Tacexpr.LtacAtomCall _) :: tail -> false | _ :: tail -> aux tail @@ -373,7 +371,7 @@ let explain_ltac_call_trace last trace loc = let skip_extensions trace = let rec aux = function | (_,Tacexpr.LtacNameCall f as tac) :: _ - when Hook.get is_for_ml_f f -> [tac] + when Tacenv.is_ltac_for_ml_tactic f -> [tac] | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac) :: _ -> [tac] | t :: tail -> t :: aux tail diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli index a3b519a71..523398e75 100644 --- a/tactics/tactic_debug.mli +++ b/tactics/tactic_debug.mli @@ -78,5 +78,3 @@ val db_breakpoint : debug_info -> val extract_ltac_trace : Tacexpr.ltac_trace -> Loc.t -> Pp.std_ppcmds option * Loc.t - -val is_ltac_for_ml_tactic_hook : (KerName.t -> bool) Hook.t diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 624636317..eebac88fb 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,4 +1,3 @@ -Tactic_debug Ftactic Geninterp Dnet @@ -22,6 +21,7 @@ Hints Auto Tacintern Tactic_matching +Tactic_debug Tacinterp Evar_tactics Term_dnet |