From 5b8432f2f7cd6a253e80f89de8a619599bec74e9 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Tue, 16 May 2017 10:38:10 +0200
Subject: [PATCH] Use return: instead of "return".

---
 theories/typing/examples/get_x.v    | 2 +-
 theories/typing/examples/lazy_lft.v | 2 +-
 theories/typing/examples/rebor.v    | 2 +-
 theories/typing/examples/unbox.v    | 2 +-
 theories/typing/lib/rc/rc.v         | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/typing/examples/get_x.v b/theories/typing/examples/get_x.v
index 59a0474a..66fef27d 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 e254f591..1efdcf94 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 1019fb9f..4efa5753 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 639017be..7b19d4be 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 1cf22bc9..d5193529 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
-- 
GitLab