search

lukaszcz / coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
218 stars 31 forks source link

Syntax error for output of hammer #144

Open skogsbaer opened 2 years ago

skogsbaer commented 2 years ago

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 commented 3 months ago

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 commented 3 months ago

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.