Use $$ rather than $ for var so as to not conflict with Ltac2 antiquotations

[JasonGross]

@andres-erbsen @samuelgruetter do you have a better way of avoiding conflicts? (bedrock2 uses prefix $ too, right?)

[JasonGross]

@jedisct1 Did something change in zig recently?

/home/runner/work/fiat-crypto/fiat-crypto/fiat-zig/src/p2[5](https://github.com/mit-plv/fiat-crypto/runs/8048429000?check_suite_focus=true#step:4:6)[6](https://github.com/mit-plv/fiat-crypto/runs/8048429000?check_suite_focus=true#step:4:7)_32.zig:61:36: error: evaluation exceeded 1000 backwards branches
/home/runner/work/fiat-crypto/fiat-crypto/fiat-zig/src/p256_32.zig:61:36: note: use @setEvalBranchQuota() to raise the branch limit from 1000
/home/runner/work/fiat-crypto/fiat-crypto/fiat-zig/src/p256_32.zig:2633:17: note: called from here

[jedisct1]

#1360 fixes this.

The root cause is still that the generated code requires a ton of extra compile-time work due to #939

[samuelgruetter]

I already complained about this a while ago, and @ppedrot's reply was that fixing this in Ltac2 would be too hard. We do use the $x notation in bedrock2 (for expr.var in source ASTs), and it seems that so far, by Requiring/Importing notations only very locally when strictly needed, and by not using Ltac2 very much, we have avoided the issue, but sooner or later, we'll run into it as well. So basically, it seems we need to accept that as soon as we Require Ltac2.Ltac2, we can't use $x and &x notations any more...

[andres-erbsen]

Actually, this seems to still work.

Require Ltac2.Ltac2.
Declare Custom Entry bedrock_expr.
Notation "bedrock_expr:( e )" := e (e custom bedrock_expr).
Notation "$ e"                := e (in custom bedrock_expr at level 0, e constr).
Check bedrock_expr:($7).

[JasonGross]

Actually, this seems to still work.

Require Ltac2.Ltac2.
Declare Custom Entry bedrock_expr.
Notation "bedrock_expr:( e )" := e (e custom bedrock_expr).
Notation "$ e"                := e (in custom bedrock_expr at level 0, e constr).
Check bedrock_expr:($7).

The issue is the other way around: reserving the notations for constr breaks Ltac2 antiqotations