diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 59a0474aadb20523bc1197e7dd2c05aed6476970..66fef27d074343423ea84d867079909a2a7fabdd 100644
--- a/theories/typing/examples/get_x.v
+++ b/theories/typing/examples/get_x.v
@@ -9,7 +9,7 @@ Section get_x.
     funrec: <> ["p"] :=
        let: "p'" := !"p" in
        letalloc: "r" <- "p'" +â‚— #0 in
-       delete [ #1; "p"] ;; "return" ["r"].
+       delete [ #1; "p"] ;; return: ["r"].
 
   Lemma get_x_type :
     typed_val get_x (fn(∀ α, ∅; &uniq{α} Π[int; int]) → &shr{α} int).
diff --git a/theories/typing/examples/lazy_lft.v b/theories/typing/examples/lazy_lft.v
index e254f5919003255fb17d7082b1236b05df6216e4..1efdcf94ca0c6a81ef5b82111e9f52d17b498fd8 100644
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -15,7 +15,7 @@ Section lazy_lft.
       let: "23" := #23 in "g" <- "23";;
       "t" +â‚— #1 <- "g";;
       let: "r" := new [ #0] in
-      Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; "return" ["r"].
+      Endlft;; delete [ #2; "t"];; delete [ #1; "f"];; delete [ #1; "g"];; return: ["r"].
 
   Lemma lazy_lft_type : typed_val lazy_lft (fn(∅) → unit).
   Proof.
diff --git a/theories/typing/examples/rebor.v b/theories/typing/examples/rebor.v
index 1019fb9f4af41fc21c5bb7cc55eb807f0398c952..4efa575329c5b7342a9457c0d3636ba428bd9d5b 100644
--- a/theories/typing/examples/rebor.v
+++ b/theories/typing/examples/rebor.v
@@ -14,7 +14,7 @@ Section rebor.
        let: "y'" := !"y" in
        letalloc: "r" <- "y'" in
        Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
-                 delete [ #1; "x"] ;; "return" ["r"].
+                 delete [ #1; "x"] ;; return: ["r"].
 
   Lemma rebor_type :
     typed_val rebor (fn(∅; Π[int; int], Π[int; int]) → int).
diff --git a/theories/typing/examples/unbox.v b/theories/typing/examples/unbox.v
index 639017be47047c71a599d3457a4759e826bce028..7b19d4be356eed375d7f2c8cade36aa1ed4f5092 100644
--- a/theories/typing/examples/unbox.v
+++ b/theories/typing/examples/unbox.v
@@ -9,7 +9,7 @@ Section unbox.
     funrec: <> ["b"] :=
        let: "b'" := !"b" in let: "bx" := !"b'" in
        letalloc: "r" <- "bx" +â‚— #0 in
-       delete [ #1; "b"] ;; "return" ["r"].
+       delete [ #1; "b"] ;; return: ["r"].
 
   Lemma ubox_type :
     typed_val unbox (fn(∀ α, ∅; &uniq{α}box (Π[int; int])) → &uniq{α} int).
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 1cf22bc9cdf42edb9e38de4e7d1c46c8bf84db81..d51935292ecf33c42203d828397242b90202b002 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -48,7 +48,7 @@ Section rc.
          authoritative state is something like (None, weak), where weak is the
          number of weak references.
        - The dead state, meaning that no reference exist anymore. The
-         authoritat state is something like (None, 0).
+         authoritative state is something like (None, 0).
 
    Note that when we are in the living or dropping states, the weak reference
    count stored in the heap is actually one plus the actual number of weak