From cfbdb375dc9092dc30ac77244dea0412e2c38483 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 22 Oct 2020 13:13:49 +0200
Subject: [PATCH] replace some 'repeat' by fixed counts

---
 theories/bi/monpred.v | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index d94391caf..f5f9e780c 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -917,17 +917,17 @@ Proof.
   - by (split=> ? /=; repeat f_equiv).
   - intros P Q [?]. split=> i /=. by do 3 f_equiv.
   - intros P. split=> i /=. by rewrite bi.forall_elim plainly_elim_persistently.
-  - intros P. split=> i /=. repeat setoid_rewrite <-plainly_forall.
+  - intros P. split=> i /=. do 3 setoid_rewrite <-plainly_forall.
     rewrite -plainly_idemp_2. f_equiv. by apply bi.forall_intro=>_.
   - intros A Ψ. split=> i /=. apply bi.forall_intro=> j.
     rewrite plainly_forall. apply bi.forall_intro=> a. by rewrite !bi.forall_elim.
-  - intros P Q. split=> i /=. repeat setoid_rewrite bi.pure_impl_forall.
-    repeat setoid_rewrite <-plainly_forall.
-    repeat setoid_rewrite bi.persistently_forall. do 4 f_equiv.
+  - intros P Q. split=> i /=. setoid_rewrite bi.pure_impl_forall.
+    setoid_rewrite <-plainly_forall.
+    do 2 setoid_rewrite bi.persistently_forall. do 4 f_equiv.
     apply persistently_impl_plainly.
   - intros P Q. split=> i /=.
-    repeat setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
-    repeat setoid_rewrite <-plainly_forall.
+    setoid_rewrite bi.pure_impl_forall. rewrite 2!bi.forall_elim //.
+    do 2 setoid_rewrite <-plainly_forall.
     setoid_rewrite plainly_impl_plainly. f_equiv.
     do 3 apply bi.forall_intro => ?. f_equiv. rewrite bi.forall_elim //.
   - intros P. split=> i /=. apply bi.forall_intro=>_. by apply plainly_emp_intro.
@@ -951,7 +951,7 @@ Qed.
 Global Instance monPred_bi_plainly_exist `{!BiPlainly PROP} `{!BiIndexBottom bot} :
   BiPlainlyExist PROP → BiPlainlyExist monPredI.
 Proof.
-  split=> ? /=. rewrite monPred_plainly_eq /=. repeat setoid_rewrite monPred_at_exist.
+  split=> ? /=. rewrite monPred_plainly_eq /=. setoid_rewrite monPred_at_exist.
   rewrite (bi.forall_elim bot) plainly_exist_1. do 2 f_equiv.
   apply bi.forall_intro=>?. by do 2 f_equiv.
 Qed.
-- 
GitLab