Merge PR #6407: Fix #6404 - Print tactics called by ML tactics

1 files changed, 2 insertions, 5 deletions

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))