Fix a broken notation.

theories/lang/lang.v

@@ -20,6 +20,7 @@ Inductive binder := BAnon | BNamed : string → binder.
 Delimit Scope lrust_binder_scope with RustB.
 Bind Scope lrust_binder_scope with binder.
 
+Notation "[ ]" := (@nil binder) : lrust_binder_scope.
 Notation "a :: b" := (@cons binder a%RustB b%RustB)
   (at level 60, right associativity) : lrust_binder_scope.
 Notation "[ x1 ; x2 ; .. ; xn ]" :=

theories/lang/lib/lock.v

@@ -2,8 +2,7 @@ From iris.program_logic Require Import weakestpre.
 From iris.base_logic.lib Require Import invariants.
 From iris.proofmode Require Import tactics.
 From iris.algebra Require Import excl.
-From lrust.lang Require Import proofmode notation.
-From lrust.lang Require Export lang.
+From lrust.lang Require Import lang proofmode notation.
 Set Default Proof Using "Type".
 
 Definition newlock : val := λ: [], let: "l" := Alloc #1 in "l" <- #false ;; "l".
@@ -54,14 +53,12 @@ Section proof.
     { iNext. iExists false. by iFrame. }
     eauto.
   Qed.
-    
 
   Lemma newlock_spec (R : iProp Σ) :
     {{{ ▷ R }}} newlock [] {{{ l γ, RET #l; is_lock γ l R }}}.
   Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
+    iIntros (Φ) "HR HΦ". iApply wp_fupd.
     wp_seq. wp_alloc l vl as "Hl" "H†". inv_vec vl=>x.
-    (* FIXME: Something is wrong with the printing of the expression here *)
     rewrite heap_mapsto_vec_singleton. (* FIXME shouldn't this also compute now, like bigops do? *)
     wp_let. wp_write.
     iMod (newlock_inplace with "[HR] Hl") as (γ) "?".

theories/lang/notation.v

@@ -12,6 +12,7 @@ Coercion Var : string >-> expr.
 Coercion BNamed : string >-> binder.
 Notation "<>" := BAnon : lrust_binder_scope.
 
+Notation "[ ]" := (@nil expr) : expr_scope.
 Notation "[ x ]" := (@cons expr x%E (@nil expr)) : expr_scope.
 Notation "[ x1 ; x2 ; .. ; xn ]" :=
   (@cons expr x1%E (@cons expr x2%E