From b907771ff46330d1b42fea1c70ed8fd689173a3f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Aug 2016 19:12:31 +0200
Subject: [PATCH] fix a comment

---
 program_logic/counter_examples.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index 3efa5311a..2f6357989 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -103,8 +103,7 @@ Module inv. Section inv.
 
   Hypothesis finished_dup : forall γ, finished γ ⊢ finished γ ★ finished γ.
 
-  (* We have that we cannot view shift from the initial state to false
-     (because the initial state is actually achievable). *)
+  (* We assume that we cannot view shift to false. *)
   Hypothesis soundness : ¬ (True ⊢ pvs1 False).
 
   (** Some general lemmas and proof mode compatibility. *)
-- 
GitLab