diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 7 |
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)) |