From 6dcae7c74bb2740675e962e631ceebbe3da489d2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Jul 2017 16:53:59 -0700
Subject: [PATCH] better explanation what goes on in panic.v

---
 theories/typing/lib/panic.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/typing/lib/panic.v b/theories/typing/lib/panic.v
index 06838ca5..5ba70deb 100644
--- a/theories/typing/lib/panic.v
+++ b/theories/typing/lib/panic.v
@@ -2,13 +2,13 @@ From iris.proofmode Require Import tactics.
 From lrust.typing Require Import typing.
 Set Default Proof Using "Type".
 
-(* Minimal support for panic. Lambdarust does not support unwinding
-   the stack. Instead, we just end the current thread by not calling
-   any continuation.
+(* Minimal support for panic. Lambdarust does not support unwinding the
+   stack. Instead, we just end the current thread by not calling any
+   continuation.
 
-   Note that this is not very faithfull, because e.g., [spawn] will
-   not be notified that the thread has finished. This is why we do not
-   get into trouble with [take_mut]. *)
+   This properly models "panic=abort", but fails to take into account the
+   trouble caused by unwinding. This is why we do not get into trouble with
+   [take_mut]. *)
 
 Section panic.
   Context `{typeG Î£}.
-- 
GitLab