Putting Tactic_debug just below Tacinterp.

8 files changed, 5 insertions, 18 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index d8fb2b906..7710033db 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -193,12 +193,12 @@ Entry
 Pcoq
 Printer
 Pptactic
-Tactic_debug
 Ppdecl_proof
 Egramml
 Egramcoq
 Tacsubst
 Tacenv
+Tactic_debug
 Trie
 Dn
 Btermdn
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