Syntax error for output of hammer

[skogsbaer]

hammer outputs:

Reconstructing the proof...
Tactic srun eauto succeeded.
Replace the hammer tactic with:
	srun eauto use: binds_neq_shrink unfold: term_subst, subst, prop_subst.

But when pasting the srun ... command into my proof script, I get a syntax error:

Error: Syntax error: [ltac_use_default] expected after [tactic] (in [tactic_command]).

Version: CoqHammer 1.3.2 for Coq 8.15

[sakekasi]

I also ran into this issue. I was able to get around this issue by writing a script that converts srun eauto use: binds_neq_shrink unfold: term_subst, subst, prop_subst. to srun (eauto) use: binds_neq_shrink unfold: term_subst, subst, prop_subst.

Adding parens seems to fix the issue

[lukaszcz]

I recall this worked with an older version of Coq. Something must've changed with Coq's parsing algorithm. I may investigate it sometime, when I find the time.