Pierre-Marie Pédrot

@coqbot run full ci

@coqbot merge now

You have to write `rewrite &eq`, otherwise you get the global constant `eq`, hence the error. It's not related to rewrite.

This behaviour is even documented [here](https://coq.inria.fr/refman/proof-engine/ltac2.html#strict-vs-non-strict-mode): > In non-strict mode, any simple identifier appearing in a term quotation which is not bound in the global environment is turned into a...

No, it's a conscious design choice. We emulate the "non-strict" Ltac1 behaviour when there is no ambiguity, but for stability of code factorization we explicitly favour the global constant over...

What is your use case?

This is definitely forbidden knowledge... Does the Ltac1 tactic notation with an integer works with a variable already? I think there is some partial support for it with the internal...

The last example doesn't test the right thing (or it's a failed test). It's not possible to pass a variable to a tactic notation expecting an integer. But that's not...

> my earlier example has demonstrated an appropriate use case Sure, sure it's not hard to implement (nor to maintain). Note that you could also just parse a constr and...

Meh. I'd rather have a unit-test per function introduced as an external, this is both simpler and more complete as a coverage test.