From f95724ab3ce96e1bb9e43ffb7ed7dcc37467cfbf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 24 Aug 2016 14:16:36 +0200
Subject: [PATCH] Remove obsolete comment.

---
 algebra/upred_big_op.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 85e2b3346..93e3c72eb 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -25,7 +25,6 @@ Instance: Params (@uPred_big_sep) 1.
 Notation "'[★]' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
 
 (** * Other big ops *)
-(** We use a type class to obtain overloaded notations *)
 Definition uPred_big_sepM {M} `{Countable K} {A}
     (m : gmap K A) (Φ : K → A → uPred M) : uPred M :=
   [★] (curry Φ <$> map_to_list m).
-- 
GitLab