From 7d197b3e6efe03946ee87a8af4694e3537d124de Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Aug 2014 22:22:04 +0200
Subject: [PATCH] Break at 80

---
 theories/list.v          | 3 ++-
 theories/listset_nodup.v | 7 +------
 theories/proof_irrel.v   | 5 -----
 3 files changed, 3 insertions(+), 12 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 1853423c..2df51d67 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2283,7 +2283,8 @@ Section Forall2.
   Proof.
     intro. unfold sublist_lookup, sublist_alter.
     erewrite <-Forall2_length by eauto; intros; simplify_option_equality.
-    apply Forall2_app_l; rewrite ?take_length_le by lia; auto using Forall2_take.
+    apply Forall2_app_l;
+      rewrite ?take_length_le by lia; auto using Forall2_take.
     apply Forall2_app_l; erewrite Forall2_length, take_length,
       drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|].
     rewrite drop_drop; auto using Forall2_drop.
diff --git a/theories/listset_nodup.v b/theories/listset_nodup.v
index b1af8fdc..b6b6af9a 100644
--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
@@ -48,12 +48,7 @@ Qed.
 
 Global Instance listset_nodup_elems: Elements A C := listset_nodup_car.
 Global Instance: FinCollection A C.
-Proof.
-  split.
-  * apply _.
-  * done.
-  * by intros [??].
-Qed.
+Proof. split. apply _. done. by intros [??]. Qed.
 Global Instance: CollectionOps A C.
 Proof.
   split.
diff --git a/theories/proof_irrel.v b/theories/proof_irrel.v
index 77b7c2c4..12e2491a 100644
--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
@@ -9,24 +9,20 @@ Instance: ProofIrrel True.
 Proof. by intros [] []. Qed.
 Instance: ProofIrrel False.
 Proof. by intros []. Qed.
-
 Instance and_pi (A B : Prop) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A ∧ B).
 Proof. intros ?? [??] [??]. by f_equal. Qed.
 Instance prod_pi (A B : Type) :
   ProofIrrel A → ProofIrrel B → ProofIrrel (A * B).
 Proof. intros ?? [??] [??]. by f_equal. Qed.
-
 Instance eq_pi {A} `{∀ x y : A, Decision (x = y)} (x y : A) :
   ProofIrrel (x = y).
 Proof.
   intros ??. apply eq_proofs_unicity.
   intros x' y'. destruct (decide (x' = y')); tauto.
 Qed.
-
 Instance Is_true_pi (b : bool) : ProofIrrel (Is_true b).
 Proof. destruct b; simpl; apply _. Qed.
-
 Lemma sig_eq_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x y : sig P) : x = y ↔ `x = `y.
 Proof.
@@ -34,7 +30,6 @@ Proof.
   destruct x as [x Hx], y as [y Hy]; simpl; intros; subst.
   f_equal. apply proof_irrel.
 Qed.
-
 Lemma exists_proj1_pi `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
   (x : sig P) p : `x ↾ p = x.
 Proof. by apply (sig_eq_pi _). Qed.
-- 
GitLab