Moving Tactic_debug to tactics/ folder.

12 files changed, 37 insertions, 45 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 34bde1ac2..d8fb2b906 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -187,13 +187,13 @@ Proofview
 Proof
 Proof_global
 Pfedit
-Tactic_debug
 Decl_mode
 Ppconstr
 Entry
 Pcoq
 Printer
 Pptactic
+Tactic_debug
 Ppdecl_proof
 Egramml
 Egramcoq
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index fdc1288ae..7d5e7772c 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1415,17 +1415,6 @@ let () =
   let printer _ _ prtac = prtac (0, E) in
   declare_extra_genarg_pprule wit_tactic printer printer printer
 
-let _ = Hook.set Tactic_debug.tactic_printer
-  (fun x -> pr_glob_tactic (Global.env()) x)
-
-let _ = Hook.set Tactic_debug.match_pattern_printer
-  (fun env sigma hyp -> pr_match_pattern (pr_constr_pattern_env env sigma) hyp)
-
-let _ = Hook.set Tactic_debug.match_rule_printer
-  (fun rl ->
-    pr_match_rule false (pr_glob_tactic (Global.env()))
-      (fun (_,p) -> pr_constr_pattern p) rl)
-
 module Richpp = struct
 
   include Make (Ppconstr.Richpp) (struct
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index c5ec6bb09..b98b6c67e 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -67,4 +67,9 @@ module type Pp = sig
     ('constr -> std_ppcmds) ->
     ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
 
+  val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+  val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+    ('b, 'a) match_rule -> std_ppcmds
+
 end
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 47a637575..08556d62e 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -11,6 +11,5 @@ Redexpr
 Refiner
 Tacmach
 Pfedit
-Tactic_debug
 Clenv
 Clenvtac
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 82252610a..36a23d580 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -44,7 +44,7 @@ open Sigma.Notations
 open Proofview.Notations
 open Context.Named.Declaration
 
-let ltac_trace_info = Tacsubst.ltac_trace_info
+let ltac_trace_info = Tactic_debug.ltac_trace_info
 
 let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
   let Val.Dyn (t, _) = v in
@@ -2201,3 +2201,16 @@ let lift_constr_tac_to_ml_tac vars tac =
     tac args ist
   end } in
   tac
+
+let vernac_debug b =
+  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "Ltac debug";
+      optkey   = ["Ltac";"Debug"];
+      optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
+      optwrite = vernac_debug }
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 17cb8ad19..55941c1ca 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -18,8 +18,6 @@ open Genredexpr
 open Patternops
 open Pretyping
 
-let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
-
 (** Substitution of tactics at module closing time *)
 
 (** For generic arguments, we declare and store substitutions
diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli
index 8b686c5ce..c1bf27257 100644
--- a/tactics/tacsubst.mli
+++ b/tactics/tacsubst.mli
@@ -11,10 +11,6 @@ open Mod_subst
 open Genarg
 open Misctypes
 
-(** TODO: Move those definitions somewhere sensible *)
-
-val ltac_trace_info : ltac_trace Exninfo.t
-
 (** Substitution of tactics at module closing time *)
 
 val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
diff --git a/proofs/tactic_debug.ml b/tactics/tactic_debug.ml
index d33278ff8..b278c371b 100644
--- a/proofs/tactic_debug.ml
+++ b/tactics/tactic_debug.ml
@@ -14,10 +14,15 @@ open Termops
 open Nameops
 open Proofview.Notations
 
-let (prtac, tactic_printer) = Hook.make ()
-let (prmatchpatt, match_pattern_printer) = Hook.make ()
-let (prmatchrl, match_rule_printer) = Hook.make ()
+let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
 
+let prtac x =
+  Pptactic.pr_glob_tactic (Global.env()) x
+let prmatchpatt env sigma hyp =
+  Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
+let prmatchrl rl =
+  Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
+    (fun (_,p) -> Printer.pr_constr_pattern p) rl
 
 (* This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
@@ -67,7 +72,7 @@ let help () =
 let goal_com tac =
   Proofview.tclTHEN
     db_pr_goal
-    (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac)))
+    (Proofview.tclLIFT (msg_tac_debug (str "Going to execute:" ++ fnl () ++ prtac tac)))
 
 (* [run (new_ref _)] gives us a ref shared among [NonLogical.t]
    expressions. It avoids parametrizing everything over a
@@ -228,7 +233,7 @@ let db_pattern_rule debug num r =
   if db then
   begin
     msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
-      str "|" ++ spc () ++ Hook.get prmatchrl r)
+      str "|" ++ spc () ++ prmatchrl r)
   end
   else return ()
 
@@ -270,7 +275,7 @@ let db_hyp_pattern_failure debug env sigma (na,hyp) =
   if db then
     msg_tac_debug (str "The pattern hypothesis" ++ hyp_bound na ++
                 str " cannot match: " ++
-           Hook.get prmatchpatt env sigma hyp)
+           prmatchpatt env sigma hyp)
   else return ()
 
 (* Prints a matching failure message for a rule *)
diff --git a/proofs/tactic_debug.mli b/tactics/tactic_debug.mli
index 215c5b29b..fbb7ab66d 100644
--- a/proofs/tactic_debug.mli
+++ b/tactics/tactic_debug.mli
@@ -13,16 +13,14 @@ open Tacexpr
 open Term
 open Evd
 
+(** TODO: Move those definitions somewhere sensible *)
+
+val ltac_trace_info : ltac_trace Exninfo.t
+
 (** This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
    complete panel of commands dedicated to a proof assistant framework *)
 
-val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t
-val match_pattern_printer :
-  (env -> evar_map -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t
-val match_rule_printer :
-  ((Tacexpr.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
-
 (** Debug information *)
 type debug_info =
   | DebugOn of int
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 2c5edc20e..624636317 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,3 +1,4 @@
+Tactic_debug
 Ftactic
 Geninterp
 Dnet
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 91ef45393..b734f075a 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -120,7 +120,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc,
       let err = Errors.make_anomaly msg in
       Util.iraise (err, info)
   in
-  let ltac_trace = Exninfo.get info Tacsubst.ltac_trace_info in
+  let ltac_trace = Exninfo.get info Tactic_debug.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with
   | None -> e
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 38832b422..d769c6033 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1433,18 +1433,6 @@ let _ =
       optread  = Flags.get_dump_bytecode;
       optwrite = Flags.set_dump_bytecode }
 
-let vernac_debug b =
-  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
-
-let _ =
-  declare_bool_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "Ltac debug";
-      optkey   = ["Ltac";"Debug"];
-      optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
-      optwrite = vernac_debug }
-
 let _ =
   declare_bool_option
     { optsync  = true;