After an upgrade to Coq 8.16, This innocuous line, `unfold set_In at 2`

gives me `Error: Syntax error: [occs_nums] expected after 'at' (in [occs]).`

The docs seem to suggest that this notation should work, and I scanned the release notes for a reference to this notation, to no avail. I'm guessing I might need to import something in order to use decimal numerals, but I tried a few things like Coq.Init.Decimal which didn't improve the situation.

How do I use `at`

in an `unfold`

tactic?

A message was moved here from #Coq users > Thinking of making a new proof editing UI by Ezra elias kilty Cooper.

Can you minimize the example? My suspicion is that the notation still works *but* you're importing some module that breaks it accidentally (it's far too easy)

That sounds promising—I'll come back with a minimal example, thanks.

OK, here is my minimal example. The defined tactic notation containing "2" interferes with the unfold ... at 2 notation, which I wouldn't really expect.

```
Tactic Notation "foo" "bar" "2" := idtac.
Lemma dilemma:
forall x y z, plus (plus x y) z = plus x (plus y z).
Proof.
unfold plus at 2.
fold plus.
Require Import Lia.
intros; lia.
Qed.
```

I do not really need to use this "clever" tactic notation with a 2, so I'll just work around it. Thanks for the suggestion, Paolo!

Oh cool it helped and thank you for the example! I knew notations could extend Coq's lexer and change the meaning of "existing" syntax, but I hadn't run into it yet with Tactic Notations!

Last updated: Oct 04 2023 at 22:01 UTC