Removing dependency of Himsg in tactic files.

6 files changed, 86 insertions, 78 deletions

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index d2d3f3117..cc87e197d 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -143,3 +143,5 @@ 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/tactic_debug.ml b/tactics/tactic_debug.ml
index b278c371b..fa40b7416 100644
--- a/tactics/tactic_debug.ml
+++ b/tactics/tactic_debug.ml
@@ -322,3 +322,81 @@ let db_breakpoint debug s =
       breakpoint:=None
   | _ ->
       return ()
+
+(** 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)
+  | (_, Tacexpr.LtacAtomCall _) :: tail ->
+      false
+  | _ :: tail -> aux tail
+  | [] -> false in
+  aux (List.rev trace)
+
+let explain_ltac_call_trace last trace loc =
+  let calls = last :: List.rev_map snd trace in
+  let pr_call ck = match ck with
+  | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn)
+  | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+  | Tacexpr.LtacMLCall t ->
+      quote (Pptactic.pr_glob_tactic (Global.env()) t)
+  | Tacexpr.LtacVarCall (id,t) ->
+      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
+        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
+  | Tacexpr.LtacAtomCall te ->
+      quote (Pptactic.pr_glob_tactic (Global.env())
+              (Tacexpr.TacAtom (Loc.ghost,te)))
+  | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
+      quote (Printer.pr_glob_constr_env (Global.env()) c) ++
+        (if not (Id.Map.is_empty vars) then
+          strbrk " (with " ++
+            prlist_with_sep pr_comma
+            (fun (id,c) ->
+                pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
+            (List.rev (Id.Map.bindings vars)) ++ str ")"
+        else mt())
+  in
+  match calls with
+  | [] -> mt ()
+  | _ ->
+    let kind_of_last_call = match List.last calls with
+    | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed."
+    | _ -> ", last call failed."
+    in
+    hov 0 (str "In nested Ltac calls to " ++
+           pr_enum pr_call calls ++ strbrk kind_of_last_call)
+
+let skip_extensions trace =
+  let rec aux = function
+  | (_,Tacexpr.LtacNameCall f as tac) :: _ 
+      when Hook.get is_for_ml_f f -> [tac]
+  | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac)
+      :: _ -> [tac]
+  | t :: tail -> t :: aux tail
+  | [] -> [] in
+  List.rev (aux (List.rev trace))
+
+let extract_ltac_trace trace eloc =
+  let trace = skip_extensions trace in
+  let (loc,c),tail = List.sep_last trace in
+  if is_defined_ltac trace then
+    (* We entered a user-defined tactic,
+       we display the trace with location of the call *)
+    let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
+    Some msg, loc
+  else
+    (* We entered a primitive tactic, we don't display trace but
+       report on the finest location *)
+    let best_loc =
+      if not (Loc.is_ghost eloc) then eloc else
+        (* trace is with innermost call coming first *)
+        let rec aux = function
+        | (loc,_)::tail when not (Loc.is_ghost loc) -> loc
+        | _::tail -> aux tail
+        | [] -> Loc.ghost in
+        aux trace in
+    None, best_loc
diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli
index fbb7ab66d..a3b519a71 100644
--- a/tactics/tactic_debug.mli
+++ b/tactics/tactic_debug.mli
@@ -75,3 +75,8 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
 (** Prints a logic failure message for a rule *)
 val db_breakpoint : debug_info ->
   Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
+
+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/toplevel/cerrors.ml b/toplevel/cerrors.ml
index b734f075a..0b8edd91c 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -126,7 +126,7 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc,
   | None -> e
   | Some trace ->
     let (e, info) = e in
-    match Himsg.extract_ltac_trace trace loc with
+    match Tactic_debug.extract_ltac_trace trace loc with
     | None, loc -> (e, Loc.add_loc info loc)
     | Some msg, loc ->
       (EvaluatedError (msg, Some e), Loc.add_loc info loc)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 1af09dd84..4ee1537c2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1244,77 +1244,3 @@ let explain_reduction_tactic_error = function
       quote (pr_goal_concl_style_env env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' Evd.empty e
-
-let is_defined_ltac trace =
-  let rec aux = function
-  | (_, Tacexpr.LtacNameCall f) :: tail ->
-      not (Tacenv.is_ltac_for_ml_tactic f)
-  | (_, Tacexpr.LtacAtomCall _) :: tail ->
-      false
-  | _ :: tail -> aux tail
-  | [] -> false in
-  aux (List.rev trace)
-
-let explain_ltac_call_trace last trace loc =
-  let calls = last :: List.rev_map snd trace in
-  let pr_call ck = match ck with
-  | Tacexpr.LtacNotationCall kn -> quote (KerName.print kn)
-  | Tacexpr.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
-  | Tacexpr.LtacMLCall t ->
-      quote (Pptactic.pr_glob_tactic (Global.env()) t)
-  | Tacexpr.LtacVarCall (id,t) ->
-      quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
-        Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
-  | Tacexpr.LtacAtomCall te ->
-      quote (Pptactic.pr_glob_tactic (Global.env())
-              (Tacexpr.TacAtom (Loc.ghost,te)))
-  | Tacexpr.LtacConstrInterp (c, { Pretyping.ltac_constrs = vars }) ->
-      quote (pr_glob_constr_env (Global.env()) c) ++
-        (if not (Id.Map.is_empty vars) then
-          strbrk " (with " ++
-            prlist_with_sep pr_comma
-            (fun (id,c) ->
-                pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
-            (List.rev (Id.Map.bindings vars)) ++ str ")"
-        else mt())
-  in
-  match calls with
-  | [] -> mt ()
-  | _ ->
-    let kind_of_last_call = match List.last calls with
-    | Tacexpr.LtacConstrInterp _ -> ", last term evaluation failed."
-    | _ -> ", last call failed."
-    in
-    hov 0 (str "In nested Ltac calls to " ++
-           pr_enum pr_call calls ++ strbrk kind_of_last_call)
-
-let skip_extensions trace =
-  let rec aux = function
-  | (_,Tacexpr.LtacNameCall f as tac) :: _ 
-      when Tacenv.is_ltac_for_ml_tactic f -> [tac]
-  | (_,(Tacexpr.LtacNotationCall _ | Tacexpr.LtacMLCall _) as tac)
-      :: _ -> [tac]
-  | t :: tail -> t :: aux tail
-  | [] -> [] in
-  List.rev (aux (List.rev trace))
-
-let extract_ltac_trace trace eloc =
-  let trace = skip_extensions trace in
-  let (loc,c),tail = List.sep_last trace in
-  if is_defined_ltac trace then
-    (* We entered a user-defined tactic,
-       we display the trace with location of the call *)
-    let msg = hov 0 (explain_ltac_call_trace c tail eloc ++ fnl()) in
-    Some msg, loc
-  else
-    (* We entered a primitive tactic, we don't display trace but
-       report on the finest location *)
-    let best_loc =
-      if not (Loc.is_ghost eloc) then eloc else
-        (* trace is with innermost call coming first *)
-        let rec aux = function
-        | (loc,_)::tail when not (Loc.is_ghost loc) -> loc
-        | _::tail -> aux tail
-        | [] -> Loc.ghost in
-        aux trace in
-    None, best_loc
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 50bbd15c6..ced54fd27 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -36,9 +36,6 @@ val explain_pattern_matching_error :
 val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
 
-val extract_ltac_trace :
-  Tacexpr.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t
-
 val explain_module_error : Modops.module_typing_error -> std_ppcmds
 
 val explain_module_internalization_error :