From 37b475da428f5d3af619751edadc5038f76d8b3a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Javier=20D=C3=ADaz?= <javier.diaz@iohk.io>
Date: Wed, 22 Nov 2023 11:55:29 -0300
Subject: [PATCH] Drop unnecessary comments

---
 src/Ouroboros-Mini_Protocols-Chain_Sync.thy | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Ouroboros-Mini_Protocols-Chain_Sync.thy b/src/Ouroboros-Mini_Protocols-Chain_Sync.thy
index 29e2ecc..0cdf319 100644
--- a/src/Ouroboros-Mini_Protocols-Chain_Sync.thy
+++ b/src/Ouroboros-Mini_Protocols-Chain_Sync.thy
@@ -177,17 +177,17 @@ corec server_program where
         Cont RequestNext \<Rightarrow>
           u \<rightarrow> C'.
           (
-            if C' = C then \<comment> \<open>no changes, continue with C\<close>
+            if C' = C then
               if b then
                 \<up> Cont (RollBackward (\<psi> (C ! k)));
                 server_program \<psi> u k False C \<phi>
               else if Suc k < length C then
                 \<up> Cont (RollForward (C ! Suc k));
                 server_program \<psi> u (Suc k) b C \<phi>
-              else \<comment> \<open>client caught up\<close>
+              else
                 \<up> Cont AwaitReply;
                 server_program \<psi> u k b C ClientCatchUp
-            else \<comment> \<open>changes found, switch to C'\<close>
+            else
               let (M', k') = chain_update_reaction \<psi> k C C' in
               \<up> Cont M';
               server_program \<psi> u k' b C' \<phi>
@@ -196,9 +196,9 @@ corec server_program where
     ClientCatchUp \<Rightarrow>
       u \<rightarrow> C'.
       (
-        if C' = C then \<comment> \<open>keep waiting for updates\<close>
+        if C' = C then
           server_program \<psi> u k b C \<phi>
-        else \<comment> \<open>changes found, switch to C'\<close>
+        else
           let (M', k') = chain_update_reaction \<psi> k C C' in
           \<up> Cont M';
           server_program \<psi> u k' b C' ClientLagging