Ltac call trace does not include tactics run by ML tactics

[JasonGross]

Version

8.7.0

Description of the problem

Ltac a _ := pose (I : I).
Ltac b _ := a ().
Ltac abs _ := transparent_abstract b ().
Ltac c _ := abs ().
Goal True.
  Fail c ().
  (* The command has indeed failed with message:
In nested Ltac calls to "c", "abs" and "transparent_abstract (tactic3)", last call
failed.
The term "I" has type "True" which should be Set, Prop or Type. *)
Abort.

I expect to see a and b in the trace.

This seems to be semi-intentional, as there is a function specifically dedicated to doing this:

coq/plugins/ltac/tactic_debug.ml

Lines 387 to 398 in 78e3385

	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 _) :: _ ->
	(* Case of an ML defined tactic with entry of the form <<"foo" args>> *)
	(* see tacextend.mlp *)
	[tac]
	| (_,Tacexpr.LtacMLCall _ as tac) :: _ -> [tac]
	| t :: tail -> t :: aux tail
	| [] -> [] in
	List.rev (aux (List.rev trace))

I think it is right to coalesce sequenced Tacexpr.LtacNotationCall and Tacexpr.LtacMLCall nodes, but wrong to skip all subsequent calls.