Fix #6404 - Print tactics called by ML tactics

5 files changed, 18 insertions, 7 deletions

diff --git a/CHANGES b/CHANGES
index 37d9d3680..3994caef6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,9 @@ Tactic language
 
 - Support for fix/cofix added in Ltac "match" and "lazymatch".
 
+- Ltac backtraces now contain include trace information about tactics
+  called by OCaml-defined tactics.
+
 Changes from 8.7.2 to 8.8+beta1
 ===============================
 
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index e55b49fb4..57a11d947 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))
diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out
index 91ceb1b58..d6056c509 100644
--- a/test-suite/output/bug5778.out
+++ b/test-suite/output/bug5778.out
@@ -1,4 +1,4 @@
 The command has indeed failed with message:
-In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call
-failed.
+In nested Ltac calls to "c", "abs", "abstract b ltac:(())", 
+"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
 The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug6404.out b/test-suite/output/bug6404.out
new file mode 100644
index 000000000..05464755f
--- /dev/null
+++ b/test-suite/output/bug6404.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)", 
+"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
+The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v
new file mode 100644
index 000000000..bbe6b1a00
--- /dev/null
+++ b/test-suite/output/bug6404.v
@@ -0,0 +1,7 @@
+Ltac a _ := pose (I : I).
+Ltac b _ := a ().
+Ltac abs _ := transparent_abstract b ().
+Ltac c _ := abs ().
+Goal True.
+  Fail c ().
+Abort.