diff --git a/theories/lang/notation.v b/theories/lang/notation.v
index bfe0a862833081b398ab0b98ec794fe0a780f716..e06e882765400d9b3241022859efcf1ea0968d7b 100644
--- a/theories/lang/notation.v
+++ b/theories/lang/notation.v
@@ -60,11 +60,12 @@ Notation "λ: xl , e" := (Lam xl%RustB e%E)
   (at level 102, xl at level 1, e at level 200) : expr_scope.
 Notation "λ: xl , e" := (locked (LamV xl%RustB e%E))
   (at level 102, xl at level 1, e at level 200) : val_scope.
-(* RJ TODO: let the user pick the name of the return continuation. *)
+
 Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%E
   (only parsing, at level 102, f, xl at level 1, e at level 200) : expr_scope.
 Notation "'funrec:' f xl := e" := (rec: f ("return"::xl) := e)%V
   (only parsing, at level 102, f, xl at level 1, e at level 200) : val_scope.
+Notation "'return:'" := "return" : expr_scope.
 
 Notation "'let:' x := e1 'in' e2" :=
   ((Lam (@cons binder x%RustB nil) e2%E) (@cons expr e1%E nil))
diff --git a/theories/typing/examples/init_prod.v b/theories/typing/examples/init_prod.v
index be375087c75d1682b85e261b7c9a6e7eddf64c32..b7da2ea5dfcc898922752ee4a5054107f1c9ba0f 100644
--- a/theories/typing/examples/init_prod.v
+++ b/theories/typing/examples/init_prod.v
@@ -10,7 +10,7 @@ Section init_prod.
        let: "x'" := !"x" in let: "y'" := !"y" in
        let: "r" := new [ #2] in
        "r" +â‚— #0 <- "x'";; "r" +â‚— #1 <- "y'";;
-       delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r"].
+       delete [ #1; "x"] ;; delete [ #1; "y"] ;; return: ["r"].
 
   Lemma init_prod_type :
     typed_val init_prod (fn([]; int, int) → Π[int;int]).
diff --git a/theories/typing/lib/cell.v b/theories/typing/lib/cell.v
index bfbe7e4a91905491e35bf52c7e601dbf53a4a711..6a729cc5d8bd9c65e5d1884d7ab78e39cbc55f87 100644
--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -82,7 +82,7 @@ Section typing.
   Arguments ty_own : simpl never.
 
   (* Constructing a cell. *)
-  Definition cell_new : val := funrec: <> ["x"] := "return" ["x"].
+  Definition cell_new : val := funrec: <> ["x"] := return: ["x"].
 
   Lemma cell_new_type ty :
     typed_val cell_new (fn([]; ty) → cell ty).
@@ -94,7 +94,7 @@ Section typing.
   Qed.
 
   (* The other direction: getting ownership out of a cell. *)
-  Definition cell_into_inner : val := funrec: <> ["x"] := "return" ["x"].
+  Definition cell_into_inner : val := funrec: <> ["x"] := return: ["x"].
 
   Lemma cell_into_inner_type ty :
     typed_val cell_into_inner (fn([]; cell ty) → ty).
@@ -106,7 +106,7 @@ Section typing.
   Qed.
 
   Definition cell_get_mut : val :=
-    funrec: <> ["x"] := "return" ["x"].
+    funrec: <> ["x"] := return: ["x"].
 
   Lemma cell_get_mut_type ty :
     typed_val cell_get_mut (fn(∀ α, [α]; &uniq{α} (cell ty)) → &uniq{α} ty).
@@ -123,7 +123,7 @@ Section typing.
     funrec: <> ["x"] :=
       let: "x'" := !"x" in
       letalloc: "r" <-{ty.(ty_size)} !"x'" in
-      delete [ #1; "x"];; "return" ["r"].
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma cell_get_type `(!Copy ty) :
     typed_val (cell_get ty) (fn(∀ α, [α]; &shr{α} (cell ty)) → ty).
@@ -143,7 +143,7 @@ Section typing.
       let: "c'" := !"c" in
       letalloc: "r" <-{ty.(ty_size)} !"c'" in
       "c'" <-{ty.(ty_size)} !"x";;
-      delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; "return" ["r"].
+      delete [ #1; "c"] ;; delete [ #ty.(ty_size); "x"] ;; return: ["r"].
 
   Lemma cell_replace_type ty :
     typed_val (cell_replace ty) (fn(∀ α, [α]; &shr{α} cell ty, ty) → ty).
diff --git a/theories/typing/lib/fake_shared_box.v b/theories/typing/lib/fake_shared_box.v
index 82ef21c14a8a6ef624da8c5dd7f6b76319dc17a8..56d4d9db28ec17517ec8137f2d93d5629a67aac7 100644
--- a/theories/typing/lib/fake_shared_box.v
+++ b/theories/typing/lib/fake_shared_box.v
@@ -7,7 +7,7 @@ Section fake_shared_box.
   Context `{typeG Σ}.
 
   Definition fake_shared_box : val :=
-    funrec: <> ["x"] := Skip ;; "return" ["x"].
+    funrec: <> ["x"] := Skip ;; return: ["x"].
 
   Lemma cell_replace_type ty :
     typed_val fake_shared_box
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 10e930a39231a85d2f813aa7aec005decd8d81c4..720310ac321e1ba174420d7ed2b931f5cf0b8495 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -15,7 +15,7 @@ Section option.
         [ "r" <-{Σ 0} ();; "k" ["r"];
           "r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
       cont: "k" ["r"] :=
-        delete [ #1; "o"];; "return" ["r"].
+        delete [ #1; "o"];; return: ["r"].
 
   Lemma option_as_mut_type Ï„ :
     typed_val
@@ -42,11 +42,11 @@ Section option.
     funrec: <> ["o"; "def"] :=
       case: !"o" of
       [ delete [ #(S Ï„.(ty_size)); "o"];;
-        "return" ["def"];
+        return: ["def"];
 
         letalloc: "r" <-{Ï„.(ty_size)} !("o" +â‚— #1) in
         delete [ #(S Ï„.(ty_size)); "o"];; delete [ #Ï„.(ty_size); "def"];;
-        "return" ["r"]].
+        return: ["r"]].
 
   Lemma option_unwrap_or_type Ï„ :
     typed_val (option_unwrap_or τ) (fn([]; option τ, τ) → τ).
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index f037596d1ef0f5686c4f264358eaebc3a7b50d11..f6b8962ffc48b4ec230a6156de319643775dd734 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -123,12 +123,12 @@ Section code.
 
   Definition rc_new ty : val :=
     funrec: <> ["x"] :=
-      let: "rcbox" := new [ #(S ty.(ty_size))] in
+      let: "rcbox" := new [ #(S ty.(ty_size)) ] in
       let: "rc" := new [ #1 ] in
       "rcbox" +â‚— #0 <- #1;;
       "rcbox" +â‚— #1 <-{ty.(ty_size)} !"x";;
       "rc" +â‚— #0 <- "rcbox";;
-      delete [ #ty.(ty_size) ; "x"];; "return" ["rc"].
+      delete [ #ty.(ty_size); "x"];; return: ["rc"].
 
   Lemma rc_new_type ty :
     typed_val (rc_new ty) (fn([]; ty) → rc ty).
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index e157512661ee7d7f58c39a3a06031cba8f6ff1d6..a7ee9b1fb11e078302523803c4508d1c72cc2275 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -50,7 +50,7 @@ Section ref_functions.
       let: "n" := !"rc" in
       "rc" <- "n" + #1;;
       letalloc: "r" <-{2} !"x'" in
-      delete [ #1; "x"];; "return" ["r"].
+      delete [ #1; "x"];; return: ["r"].
 
   (* FIXME : using λ instead of fun triggers an anomaly.
      See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
@@ -112,7 +112,7 @@ Section ref_functions.
       let: "x'" := !"x" in
       let: "r'" := !"x'" in
       letalloc: "r" <- "r'" in
-      delete [ #1; "x"];; "return" ["r"].
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma ref_deref_type ty :
     typed_val ref_deref
@@ -150,7 +150,7 @@ Section ref_functions.
       "rc" <- "n" - #1;;
       Endlft;;
       delete [ #2; "x"];;
-      let: "r" := new [ #0] in "return" ["r"].
+      let: "r" := new [ #0] in return: ["r"].
 
   Lemma ref_drop_type ty :
     typed_val ref_drop (fn(∀ α, [α]; ref α ty) → unit).
@@ -214,7 +214,7 @@ Section ref_functions.
       "ref" <- "r'";;
       delete [ #1; "f"];; "k" []
     cont: "k" [] :=
-      "return" ["ref"].
+      return: ["ref"].
 
   Lemma ref_map_type ty1 ty2 envty E :
     typed_val ref_map
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 91f67707ed9ce0c4aa9c1f4519adc08da4d9b767..c5b433be50458c4dd3fc08b5d6fe87ac83a6899d 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -17,7 +17,7 @@ Section refcell_functions.
       let: "r" := new [ #(S ty.(ty_size))] in
       "r" +â‚— #0 <- #0;;
       "r" +â‚— #1 <-{ty.(ty_size)} !"x";;
-      delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
+      delete [ #ty.(ty_size) ; "x"];; return: ["r"].
 
   Lemma refcell_new_type ty :
     typed_val (refcell_new ty) (fn([]; ty) → refcell ty).
@@ -54,7 +54,7 @@ Section refcell_functions.
       "r" <-{ty.(ty_size)} !("x" +â‚— #1);;
           (* TODO RJ: Can we make it so that the parenthesis above are mandatory?
              Leaving them away is inconsistent with `let ... := !"x" +â‚— #1`. *)
-       delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
+       delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
 
   Lemma refcell_into_inner_type ty :
     typed_val (refcell_into_inner ty) (fn([]; refcell ty) → ty).
@@ -88,7 +88,7 @@ Section refcell_functions.
     funrec: <> ["x"] :=
       let: "x'" := !"x" in
       "x" <- "x'" +â‚— #1;;
-      "return" ["x"].
+      return: ["x"].
 
   Lemma refcell_get_mut_type ty :
     typed_val refcell_get_mut (fn(∀ α, [α]; &uniq{α} (refcell ty)) → &uniq{α} ty)%T.
@@ -137,7 +137,7 @@ Section refcell_functions.
         delete [ #2; "ref"];;
         "k" ["r"]
       cont: "k" ["r"] :=
-        delete [ #1; "x"];; "return" ["r"].
+        delete [ #1; "x"];; return: ["r"].
 
   Lemma refcell_try_borrow_type ty :
     typed_val refcell_try_borrow (fn(∀ α, [α] ; &shr{α}(refcell ty)) → option (ref α ty)).
@@ -241,7 +241,7 @@ Section refcell_functions.
         "r" <-{Σ 0} ();;
         "k" ["r"]
       cont: "k" ["r"] :=
-        delete [ #1; "x"];; "return" ["r"].
+        delete [ #1; "x"];; return: ["r"].
 
   Lemma refcell_try_borrow_mut_type ty :
     typed_val refcell_try_borrow_mut
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index a9534a10e51930405315fe9e7f6971ba851c2db7..c5039c184e0e7c64a4f5e00d94ac84c0302cee1a 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -16,7 +16,7 @@ Section refmut_functions.
       let: "x'" := !"x" in
       let: "r'" := !"x'" in
       letalloc: "r" <- "r'" in
-      delete [ #1; "x"];; "return" ["r"].
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma refmut_deref_type ty :
     typed_val refmut_deref
@@ -56,7 +56,7 @@ Section refmut_functions.
       let: "x'" := !"x" in
       let: "r'" := !"x'" in
       letalloc: "r" <- "r'" in
-      delete [ #1; "x"];; "return" ["r"].
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma refmut_derefmut_type ty :
     typed_val refmut_derefmut
@@ -111,7 +111,7 @@ Section refmut_functions.
       "rc" <- #0;;
       Endlft;;
       delete [ #2; "x"];;
-      let: "r" := new [ #0] in "return" ["r"].
+      let: "r" := new [ #0] in return: ["r"].
 
   Lemma refmut_drop_type ty :
     typed_val refmut_drop (fn(∀ α, [α]; refmut α ty) → unit).
@@ -164,7 +164,7 @@ Section refmut_functions.
       "ref" <- "r'";;
       delete [ #1; "f"];; "k" []
     cont: "k" [] :=
-      "return" ["ref"].
+      return: ["ref"].
 
   Lemma refmut_map_type ty1 ty2 envty E :
     typed_val refmut_map
diff --git a/theories/typing/lib/rwlock/rwlock_code.v b/theories/typing/lib/rwlock/rwlock_code.v
index 2a6caa17c1cfb08d21ca1a7ca236e7b5aa2368a5..18b83f2536ff2860e1058ce4eb206fe968bfe046 100644
--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -17,7 +17,7 @@ Section rwlock_functions.
       let: "r" := new [ #(S ty.(ty_size))] in
       "r" +â‚— #0 <- #0;;
       "r" +â‚— #1 <-{ty.(ty_size)} !"x";;
-       delete [ #ty.(ty_size) ; "x"];; "return" ["r"].
+       delete [ #ty.(ty_size) ; "x"];; return: ["r"].
 
   Lemma rwlock_new_type ty :
     typed_val (rwlock_new ty) (fn([]; ty) → rwlock ty).
@@ -53,7 +53,7 @@ Section rwlock_functions.
     funrec: <> ["x"] :=
       let: "r" := new [ #ty.(ty_size)] in
       "r" <-{ty.(ty_size)} !("x" +â‚— #1);;
-       delete [ #(S ty.(ty_size)) ; "x"];; "return" ["r"].
+       delete [ #(S ty.(ty_size)) ; "x"];; return: ["r"].
 
   Lemma rwlock_into_inner_type ty :
     typed_val (rwlock_into_inner ty) (fn([] ; rwlock ty) → ty).
@@ -87,7 +87,7 @@ Section rwlock_functions.
     funrec: <> ["x"] :=
       let: "x'" := !"x" in
       "x" <- "x'" +â‚— #1;;
-      "return" ["x"].
+      return: ["x"].
 
   Lemma rwlock_get_mut_type ty :
     typed_val rwlock_get_mut (fn(∀ α, [α]; &uniq{α} (rwlock ty)) → &uniq{α} ty).
@@ -135,7 +135,7 @@ Section rwlock_functions.
              "k" ["r"]
            else "loop" [])
       cont: "k" ["r"] :=
-        delete [ #1; "x"];; "return" ["r"].
+        delete [ #1; "x"];; return: ["r"].
 
   Lemma rwlock_try_read_type ty :
     typed_val rwlock_try_read
@@ -250,7 +250,7 @@ Section rwlock_functions.
         "r" <-{Σ 0} ();;
         "k" ["r"]
       cont: "k" ["r"] :=
-        delete [ #1; "x"];; "return" ["r"].
+        delete [ #1; "x"];; return: ["r"].
 
   Lemma rwlock_try_write_type ty :
     typed_val rwlock_try_write
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 353f6b7215815afc23ad4543e1ae62175832b6b9..967055edd80749b81fbee9fb021cc6058399d6e5 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -16,7 +16,7 @@ Section rwlockreadguard_functions.
       let: "x'" := !"x" in
       let: "r'" := !"x'" +â‚— #1 in
       letalloc: "r" <- "r'" in
-      delete [ #1; "x"];; "return" ["r"].
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma rwlockreadguard_deref_type ty :
     typed_val rwlockreadguard_deref
@@ -56,7 +56,7 @@ Section rwlockreadguard_functions.
          let: "n" := !ˢᶜ"x'" in
          if: CAS "x'" "n" ("n" - #1) then
            delete [ #1; "x"];;
-           let: "r" := new [ #0] in "return" ["r"]
+           let: "r" := new [ #0] in return: ["r"]
          else "loop" []).
 
   Lemma rwlockreadguard_drop_type ty :
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 68741c9e7c2204cac8d3abebcd6bc94c233cd2b5..e652202a9abb33ad59ea5edfa516326e32030a0b 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -16,7 +16,7 @@ Section rwlockwriteguard_functions.
       let: "x'" := !"x" in
       let: "r'" := !"x'" +â‚— #1 in
       letalloc: "r" <- "r'" in
-      delete [ #1; "x"];; "return" ["r"].
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma rwlockwriteguard_deref_type ty :
     typed_val rwlockwriteguard_deref
@@ -58,7 +58,7 @@ Section rwlockwriteguard_functions.
       let: "x'" := !"x" in
       let: "r'" := !"x'" +â‚— #1 in
       letalloc: "r" <- "r'" in
-      delete [ #1; "x"];; "return" ["r"].
+      delete [ #1; "x"];; return: ["r"].
 
   Lemma rwlockwriteguard_derefmut_type ty :
     typed_val rwlockwriteguard_derefmut
@@ -105,7 +105,7 @@ Section rwlockwriteguard_functions.
       let: "x'" := !"x" in
       "x'" <-ˢᶜ #0;;
       delete [ #1; "x"];;
-      let: "r" := new [ #0] in "return" ["r"].
+      let: "r" := new [ #0] in return: ["r"].
 
   Lemma rwlockwriteguard_drop_type ty :
     typed_val rwlockwriteguard_drop
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 390d44c3ce478a14e5f56bbc8ccf1922e56a2ce6..9b4d2ebb7c552ecb11ced0fb6a2dfaac27322083 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -65,7 +65,7 @@ Section spawn.
                             letcall: "r" := "f'" ["env":expr] in
                             finish ["c"; "r"]] in
       letalloc: "r" <- "join" in
-      delete [ #1; "f"];; "return" ["r"].
+      delete [ #1; "f"];; return: ["r"].
 
   Lemma spawn_type `(!Send envty, !Send retty) :
     typed_val spawn (fn([]; fn([] ; envty) → retty, envty) → join_handle retty).
@@ -111,7 +111,7 @@ Section spawn.
     funrec: <> ["c"] :=
       let: "c'" := !"c" in
       let: "r" := join ["c'"] in
-      delete [ #1; "c"];; "return" ["r"].
+      delete [ #1; "c"];; return: ["r"].
 
   Lemma join_type retty :
     typed_val join (fn([]; join_handle retty) → retty).