Fix more notations

theories/examples/queue/code_hw.v

@@ -56,7 +56,7 @@ Section HW_queue.
                            ["q" +ₗ (#buff + "j"); #0] in
           if: "x" = #0
           then "loop" ["i" - #1]
-          else (Var "x")
+          else "x"
     .
 
   (* Dequeue also only fails when the buffer is full.

theories/examples/stack/code_elimination.v

@@ -50,13 +50,10 @@ Section elim_stack.
         (* can return CANCELLED (= FAIL_RACE) or a real element *)
         let: "e" := exchange ["ex"; #DUMMY_XCHG] in
         if: #0 < "e"
-        then
-          (* only succeeds with a 0 < return *)
-          (Var "e")
+        then "e" (* only succeeds with a 0 < return *)
         else (* exchange fails, or we accidentally exchanged with another pop *)
           #FAIL_RACE
-      else
-        (Var "v") (* can return EMPTY or a real element *)
+      else "v" (* can return EMPTY or a real element *)
     .
 
   (** Similar to Treiber stack's [pop] *)
@@ -65,6 +62,6 @@ Section elim_stack.
       let: "v" := try_pop ["es"] in
       if: "v" = #FAIL_RACE
       then "try" ["es"] (* retry if FAIL_RACE *)
-      else (Var "v") (* can return EMPTY or a real element *)
+      else "v" (* can return EMPTY or a real element *)
     .
 End elim_stack.