From 2b560f64b12dd1173e2c4a043c071c5113f37b5a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Wed, 1 Dec 2021 16:59:09 +0000
Subject: [PATCH] style nits

---
 theories/list.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index ced9cd77..3e24e703 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -4284,8 +4284,8 @@ Section permutations.
   Qed.
 End permutations.
 
-(** ** Properties of the folding functions
-Note that [foldr] has much better support, so when in doubt, it should be
+(** ** Properties of the folding functions *)
+(** Note that [foldr] has much better support, so when in doubt, it should be
 preferred over [foldl]. *)
 Definition foldr_app := @fold_right_app.
 Lemma foldr_snoc {A B} (f : B → A → A) (a : A) l x :
@@ -4330,14 +4330,14 @@ Proof.
 Qed.
 Lemma foldr_cons_permute {A} (R : relation A) `{!PreOrder R}
     (f : A → A → A) (a : A) `{!∀ a, Proper (R ==> R) (f a), !Assoc R f, !Comm R f} x l :
-  R (foldr f a (x::l)) (foldr f (f x a) l).
+  R (foldr f a (x :: l)) (foldr f (f x a) l).
 Proof.
   rewrite <-foldr_snoc.
   eapply foldr_permutation_proper'; [done..|].
   rewrite Permutation_app_comm. done.
 Qed.
 Lemma foldr_cons_permute_eq {A} (f : A → A → A) (a : A) `{!Assoc (=) f, !Comm (=) f} x l :
-  foldr f a (x::l) = foldr f (f x a) l.
+  foldr f a (x :: l) = foldr f (f x a) l.
 Proof. eapply (foldr_cons_permute eq); apply _. Qed.
 
 Lemma foldl_app {A B} (f : A → B → A) (l k : list B) (a : A) :
-- 
GitLab