From edcdbaec80fb1f5844a6738939f7da7f540868e0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 10 Mar 2017 10:14:38 +0100
Subject: [PATCH] *oops* undo accidental changes
---
theories/typing/lib/option.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index 9ebe8045..720310ac 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"].
--
GitLab