diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 9ebe8045f995c14dbd99724e7d8bbe93ea18d442..720310ac321e1ba174420d7ed2b931f5cf0b8495 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -12,8 +12,8 @@ Section option.
       let: "o'" := !"o" in
       let: "r" := new [ #2 ] in
       case: !"o'" of
-        [ "r" <-{Σ 0} ();; "k" [];
-          "r" <-{Σ 1} "o'" +ₗ #1;; "k" [] ]
+        [ "r" <-{Σ 0} ();; "k" ["r"];
+          "r" <-{Σ 1} "o'" +ₗ #1;; "k" ["r"] ]
       cont: "k" ["r"] :=
         delete [ #1; "o"];; return: ["r"].