From d9a7712b231f92882c2dccdc62d24ea3109abb0e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 12 Dec 2017 13:52:42 -0500
Subject: Fix #6404 - Print tactics called by ML tactics

---
 plugins/ltac/tactic_debug.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index e55b49fb4e..57a11d9477 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -391,13 +391,10 @@ let explain_ltac_call_trace last trace loc =
 
 let skip_extensions trace =
   let rec aux = function
-  | (_,Tacexpr.LtacNameCall f as tac) :: _
-       when Tacenv.is_ltac_for_ml_tactic f -> [tac]
-  | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: _ ->
+  | (_,Tacexpr.LtacNotationCall _ as tac) :: (_,Tacexpr.LtacMLCall _) :: tail ->
      (* Case of an ML defined tactic with entry of the form <<"foo" args>> *)
      (* see tacextend.mlp *)
-     [tac]
-  | (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac]
+     tac :: aux tail
   | t :: tail -> t :: aux tail
   | [] -> [] in
   List.rev (aux (List.rev trace))
-- 
cgit v1.2.3