From bc055a22271e70475891a4362dbac376e8b9a24b Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 6 May 2020 20:51:51 +0200
Subject: [PATCH] Removed dangling `-` that somehow did not cause compilation
 errors

---
 theories/channel/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 90e2817..52bf7ef 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -12,7 +12,7 @@ From iris.proofmode Require Export tactics.
 From actris Require Export channel.
 From iris.proofmode Require Import coq_tactics reduction spec_patterns.
 
--(** * Tactics for proving contractiveness of protocols *)
+(** * Tactics for proving contractiveness of protocols *)
 Ltac f_dist_le :=
   match goal with
   | H : _ ≡{?n}≡ _ |- _ ≡{?n'}≡ _ => apply (dist_le n); [apply H|lia]
-- 
GitLab