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.