Use $$ instead of $ to avoid Ltac2 conflict (#55)

src/Rewriter/Language/Language.v

@@ -548,7 +548,7 @@ Module Compilers.
       Notation "\ x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope.
       Notation "'λ' x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope.
       Notation "'expr_let' x := A 'in' b" := (LetIn A (fun x => b%expr)) : expr_scope.
-      Notation "'$' x" := (Var x) : expr_scope.
+      Notation "'$$' x" := (Var x) : expr_scope.
       Notation "### x" := (Ident x) : expr_scope.
     End Notations.
   End expr.

src/Rewriter/Language/UnderLets.v

@@ -22,13 +22,13 @@ Module Compilers.
                     let eC' := fun v => @subst_var_like tC (eC v) in
                     if is_var_like _ ex'
                     then eC' ex'
-                    else expr.LetIn ex' (fun v => eC' ($v))
+                    else expr.LetIn ex' (fun v => eC' ($$v))
                | expr.App s d f x
                  => let f' := @subst_var_like _ f in
                     let x' := @subst_var_like _ x in
                     expr.App f' x'
                | expr.Abs s d f
-                 => expr.Abs (fun v => @subst_var_like _ (f ($v)))
+                 => expr.Abs (fun v => @subst_var_like _ (f ($$v)))
                | expr.Var t v => v
                | expr.Ident t idc => expr.Ident idc
                end%expr.
@@ -177,10 +177,10 @@ Module Compilers.
         Let default_reify_and_let_binds_base_cps {t : base_type} : expr t -> forall T, (expr t -> UnderLets T) -> UnderLets T
           := fun e T k
              => match invert_expr.invert_Var e with
-                | Some v => k ($v)%expr
+                | Some v => k ($$v)%expr
                 | None => if is_var_like e
                           then k e
-                          else UnderLets.UnderLet e (fun v => k ($v)%expr)
+                          else UnderLets.UnderLet e (fun v => k ($$v)%expr)
                 end.
 
         Fixpoint reify_and_let_binds_base_cps {t : base_type} : expr t -> forall T, (expr t -> UnderLets T) -> UnderLets T
@@ -253,7 +253,7 @@ Module Compilers.
                                           d
                                           match invert_Abs e with
                                           | Some f => f v
-                                          | None => e @ $v
+                                          | None => e @ $$v
                                           end%expr)
              end.
       End with_var.

src/Rewriter/Language/UnderLetsProofs.v

@@ -1602,7 +1602,7 @@ Module Compilers.
                          | solve [ wf_t ]
                          | match goal with
                            | [ H : _ |- expr.interp _ (let_bind_return _ ?e0) == expr.interp _ ?e ?v ]
-                             => eapply (H e0 (e @ $v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ]
+                             => eapply (H e0 (e @ $$v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ]
                            | [ H : _ |- expr.interp _ (let_bind_return _ ?e0) == expr.interp _ ?e ?v ]
                              => cbn [expr.interp]; eapply H; [ | solve [ wf_t ] ]; solve [ wf_t ]
                            end ];

src/Rewriter/Rewriter/ProofsCommon.v

@@ -1744,8 +1744,8 @@ Module Compilers.
                 | specialize (fun with_lets G => @wf_reify with_lets G d); specialize (fun with_lets G => wf_reflect with_lets G s) ].
               { destruct with_lets; cbn; intros; auto using UnderLets.wf_to_expr. }
               { intros e1 e2 Hwf.
-                change (reify e1) with (λ x, @reify _ _ d (e1 (@reflect _ _ s ($x))))%expr.
-                change (reify e2) with (λ x, @reify _ _ d (e2 (@reflect _ _ s ($x))))%expr.
+                change (reify e1) with (λ x, @reify _ _ d (e1 (@reflect _ _ s ($$x))))%expr.
+                change (reify e2) with (λ x, @reify _ _ d (e2 (@reflect _ _ s ($$x))))%expr.
                 constructor; intros; eapply wf_reify, Hwf with (seg:=cons _ nil); [ | eapply wf_reflect; constructor ]; wf_t. } }
             { destruct t as [t|s d];
                 [ clear wf_reflect wf_reify
@@ -3204,7 +3204,7 @@ Module Compilers.
                        | [ |- expr.wf ?seg (#_) (#_) ]
                          => (tryif is_evar seg then instantiate (1:=nil) else idtac);
                             constructor
-                       | [ |- expr.wf _ ($_) ($_) ] => constructor
+                       | [ |- expr.wf _ ($$_) ($$_) ] => constructor
                        | [ |- expr.wf _ (expr.Abs _) (expr.Abs _) ] => constructor; intros
                        | [ |- expr.wf _ (UnderLets.to_expr _) (UnderLets.to_expr _) ] => apply UnderLets.wf_to_expr
                        | [ H : expr.wf ?G ?x ?y |- expr.wf ?seg ?x ?y ] => first [ is_evar seg | constr_eq G seg ]; exact H

src/Rewriter/Rewriter/ProofsCommonTactics.v

@@ -112,7 +112,7 @@ Module Compilers.
                      | match goal with
                        | [ |- expr.wf _ (_ @ _) (_ @ _) ] => constructor
                        | [ |- expr.wf _ (#_) (#_) ] => constructor
-                       | [ |- expr.wf _ ($_) ($_) ] => constructor
+                       | [ |- expr.wf _ ($$_) ($$_) ] => constructor
                        | [ |- expr.wf _ (expr.Abs _) (expr.Abs _) ] => constructor; intros
                        | [ H : @List.In ?T _ ?ls |- _ ] => is_evar ls; unify ls (@nil T); cbn [List.In] in H
                        | [ |- List.In ?v ?ls ] => is_evar ls; instantiate (1:=cons v _)

src/Rewriter/Rewriter/Rewriter.v

@@ -519,7 +519,7 @@ Module Compilers.
              | type.base _, true => fun v => UnderLets.to_expr v
              | type.arrow s d, _
                => fun f
-                  => λ x , @reify _ d (f (@reflect _ s ($x)))
+                  => λ x , @reify _ d (f (@reflect _ s ($$x)))
              end%expr%under_lets%cps
         with reflect {with_lets} {t} : expr t -> value' with_lets t
              := match t, with_lets return expr t -> value' with_lets t with

src/Rewriter/Util/Notations.v

@@ -116,8 +116,6 @@ Reserved Notation "≤" (at level 71).
 Reserved Notation "≥" (at level 71).
 Reserved Notation "a !== b" (at level 70, no associativity).
 Reserved Notation "a ≢ b" (at level 70, no associativity).
-Reserved Notation "$$ v" (at level 40).
-Reserved Notation "& x" (at level 30).
 Reserved Notation "** x" (at level 30).
 Reserved Notation "A <- X ; B" (at level 70, X at next level, right associativity, format "'[v' A  <-  X ; '/' B ']'").
 Reserved Notation "A <-- X ; B" (at level 70, X at next level, right associativity, format "'[v' A  <--  X ; '/' B ']'").
@@ -188,7 +186,8 @@ Reserved Notation "A ~> R" (at level 99).
 Reserved Notation "A --->" (left associativity, at level 65).
 Reserved Notation "'return' x" (at level 70, format "'return'  x").
 Reserved Notation "f x" (only printing, at level 10, left associativity).
-Reserved Notation "$ x" (at level 9, x at level 9, format "$ x").
+(* N.B. $ x conflicts with Ltac2's antiquotations, cf https://coq.inria.fr/refman/proof-engine/ltac2.html#dynamic-semantics *)
+Reserved Notation "$$ x" (at level 9, x at level 9, format "$$ x").
 Reserved Notation "# x" (at level 9, x at level 9, format "# x").
 Reserved Notation "## x" (at level 9, x at level 9, format "## x").
 Reserved Notation "### x" (at level 9, x at level 9, format "### x").