File "stdin", line 5, characters 0-3:
Warning: Tactic foo is deprecated since X.Y. Use idtac instead.
[deprecated-tactic,deprecated]