The proof below fails with the error:
"Error: Syntax error: [tactic:red_expr] expected after 'eval' (in [tactic:constr_eval])."
In the example below, “eval” is sometimes parsed using my definition and sometimes not, in ways that I cannot predict.
Am I doing something wrong or is this a bug in the parser?
Set Default Proof Using "Type". Ltac mytac k := rewrite (plus_O_n k). Definition eval2 := 2 . Definition eval := 3. Lemma test_mytac_eval: 0 + eval = eval. Proof. assert(0 + eval = eval) by (rewrite plus_O_n; auto). assert(0 + eval2 = eval2) by (mytac eval2; reflexivity). mytac eval. reflexivity. Qed.