From 8fc1b24bf76d31309b0f18e731c1289f295f682a Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Tue, 31 Mar 2020 09:00:27 +0200
Subject: [PATCH] remove trailing whitespace

This was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.
---
 theories/base.v      |  4 ++--
 theories/boolset.v   |  2 +-
 theories/fin_maps.v  |  2 +-
 theories/gmultiset.v |  2 +-
 theories/hashset.v   |  2 +-
 theories/lexico.v    |  2 +-
 theories/list.v      | 16 ++++++++--------
 theories/listset.v   |  2 +-
 theories/numbers.v   |  4 ++--
 theories/sets.v      |  4 ++--
 theories/tactics.v   |  2 +-
 11 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 0e6fece3..c972c3f2 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1000,7 +1000,7 @@ Hint Mode UpClose - ! : typeclass_instances.
 Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
-(** We define operational type classes for the monadic operations bind, join 
+(** We define operational type classes for the monadic operations bind, join
 and fmap. We use these type classes merely for convenient overloading of
 notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
@@ -1106,7 +1106,7 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [partial_alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value at key [k] or [None]
-if [k] is not a member of [m]. The value at [k] should be deleted if [f] 
+if [k] is not a member of [m]. The value at [k] should be deleted if [f]
 yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
diff --git a/theories/boolset.v b/theories/boolset.v
index 8a0d4c54..d630688e 100644
--- a/theories/boolset.v
+++ b/theories/boolset.v
@@ -24,7 +24,7 @@ Proof.
   - by intros x y; rewrite <-(bool_decide_spec (x = y)).
   - split. apply orb_prop_elim. apply orb_prop_intro.
   - split. apply andb_prop_elim. apply andb_prop_intro.
-  - intros X Y x; unfold elem_of, boolset_elem_of; simpl. 
+  - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
     destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
   - done.
 Qed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d8d65511..eaab32fe 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -41,7 +41,7 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
   elem_of_map_to_list {A} (m : M A) i x :
     (i,x) ∈ map_to_list m ↔ m !! i = Some x;
   lookup_omap {A B} (f : A → option B) (m : M A) i :
-    omap f m !! i = m !! i ≫= f; 
+    omap f m !! i = m !! i ≫= f;
   lookup_merge {A B C} (f : option A → option B → option C)
       `{!DiagNone f} (m1 : M A) (m2 : M B) i :
     merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 634b010a..f0fa7ffb 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -50,7 +50,7 @@ Section definitions.
 
   Global Instance gmultiset_dom : Dom (gmultiset A) (gset A) := λ X,
     let (X) := X in dom _ X.
-End definitions. 
+End definitions.
 
 Typeclasses Opaque gmultiset_elem_of gmultiset_subseteq.
 Typeclasses Opaque gmultiset_elements gmultiset_size gmultiset_empty.
diff --git a/theories/hashset.v b/theories/hashset.v
index cb1f86aa..ba2e173f 100644
--- a/theories/hashset.v
+++ b/theories/hashset.v
@@ -29,7 +29,7 @@ Next Obligation.
 Qed.
 Global Program Instance hashset_union: Union (hashset hash) := λ m1 m2,
   let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
-  Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _. 
+  Hashset (union_with (λ l k, Some (list_union l k)) m1 m2) _.
 Next Obligation.
   intros _ _ m1 Hm1 m2 Hm2 n l'; rewrite lookup_union_with_Some.
   intros [[??]|[[??]|(l&k&?&?&?)]]; simplify_eq/=; auto.
diff --git a/theories/lexico.v b/theories/lexico.v
index 87106373..6c051421 100644
--- a/theories/lexico.v
+++ b/theories/lexico.v
@@ -141,7 +141,7 @@ Instance sig_lexico_po `{Lexico A, !StrictOrder (@lexico A _)}
   (P : A → Prop) `{∀ x, ProofIrrel (P x)} : StrictOrder (@lexico (sig P) _).
 Proof.
   unfold lexico, sig_lexico. split.
-  - intros [x ?] ?. by apply (irreflexivity lexico x). 
+  - intros [x ?] ?. by apply (irreflexivity lexico x).
   - intros [x1 ?] [x2 ?] [x3 ?] ??. by trans x2.
 Qed.
 Instance sig_lexico_trichotomy `{Lexico A, tA : !TrichotomyT (@lexico A _)}
diff --git a/theories/list.v b/theories/list.v
index 2a2a7946..0cb74cf5 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -401,7 +401,7 @@ used by [positives_flatten]. *)
 Definition positives_unflatten (p : positive) : option (list positive) :=
   positives_unflatten_go p [] 1.
 
-(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1] 
+(** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1]
 over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **)
 Definition seqZ (m len: Z) : list Z :=
   (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)).
@@ -4144,7 +4144,7 @@ Section positives_flatten_unflatten.
       rewrite 2!(assoc_L (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_go_app p suffix xs acc :
     positives_unflatten_go (suffix ++ Preverse (Pdup p)) xs acc =
     positives_unflatten_go suffix xs (acc ++ p).
@@ -4161,7 +4161,7 @@ Section positives_flatten_unflatten.
       reflexivity.
     - reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_flatten_go suffix xs acc :
     positives_unflatten_go (suffix ++ positives_flatten_go xs 1) acc 1 =
     positives_unflatten_go suffix (xs ++ acc) 1.
@@ -4178,7 +4178,7 @@ Section positives_flatten_unflatten.
       rewrite (left_id_L 1 (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_unflatten_flatten xs :
     positives_unflatten (positives_flatten xs) = Some xs.
   Proof.
@@ -4191,7 +4191,7 @@ Section positives_flatten_unflatten.
     rewrite (right_id_L [] (++)%list).
     reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_app xs ys :
     positives_flatten (xs ++ ys) = positives_flatten xs ++ positives_flatten ys.
   Proof.
@@ -4205,7 +4205,7 @@ Section positives_flatten_unflatten.
       rewrite (assoc_L (++)).
       reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_cons x xs :
     positives_flatten (x :: xs) = 1~1~0 ++ Preverse (Pdup x) ++ positives_flatten xs.
   Proof.
@@ -4214,7 +4214,7 @@ Section positives_flatten_unflatten.
     rewrite (assoc_L (++)).
     reflexivity.
   Qed.
-  
+
   Lemma positives_flatten_suffix (l k : list positive) :
     l `suffix_of` k → ∃ q, positives_flatten k = q ++ positives_flatten l.
   Proof.
@@ -4222,7 +4222,7 @@ Section positives_flatten_unflatten.
     exists (positives_flatten l').
     apply positives_flatten_app.
   Qed.
-  
+
   Lemma positives_flatten_suffix_eq p1 p2 (xs ys : list positive) :
     length xs = length ys →
     p1 ++ positives_flatten xs = p2 ++ positives_flatten ys →
diff --git a/theories/listset.v b/theories/listset.v
index c443682b..2e0e892c 100644
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -29,7 +29,7 @@ Proof.
   destruct X as [l]; split; [|by intros; simplify_eq/=].
   rewrite elem_of_equiv_empty; intros Hl.
   destruct l as [|x l]; [done|]. feed inversion (Hl x). left.
-Qed. 
+Qed.
 Global Instance listset_empty_dec (X : listset A) : Decision (X ≡ ∅).
 Proof.
  refine (cast_if (decide (listset_car X = [])));
diff --git a/theories/numbers.v b/theories/numbers.v
index 44d57e3f..330dcf47 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -213,7 +213,7 @@ Proof.
   - by rewrite Preverse_xO, Preverse_app, IH.
   - reflexivity.
 Qed.
-    
+
 Instance Preverse_inj : Inj (=) (=) Preverse.
 Proof.
   intros p q eq.
@@ -571,7 +571,7 @@ Proof.
   by apply Qcplus_le_mono_l.
 Qed.
 Lemma Qcplus_nonneg_pos (x y : Qc) : 0 ≤ x → 0 < y → 0 < x + y.
-Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed. 
+Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed.
 Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y.
 Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
 Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
diff --git a/theories/sets.v b/theories/sets.v
index 3ecda91d..5e63b40a 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -564,7 +564,7 @@ Section semi_set.
     Lemma union_list_reverse_L Xs : ⋃ (reverse Xs) = ⋃ Xs.
     Proof. unfold_leibniz. apply union_list_reverse. Qed.
     Lemma empty_union_list_L Xs : ⋃ Xs = ∅ ↔ Forall (.= ∅) Xs.
-    Proof. unfold_leibniz. by rewrite empty_union_list. Qed. 
+    Proof. unfold_leibniz. by rewrite empty_union_list. Qed.
   End leibniz.
 
   Lemma not_elem_of_iff `{!RelDecision (∈@{C})} X Y x :
@@ -604,7 +604,7 @@ Section set.
 
   (** Intersection *)
   Lemma subseteq_intersection X Y : X ⊆ Y ↔ X ∩ Y ≡ X.
-  Proof. set_solver. Qed. 
+  Proof. set_solver. Qed.
   Lemma subseteq_intersection_1 X Y : X ⊆ Y → X ∩ Y ≡ X.
   Proof. apply subseteq_intersection. Qed.
   Lemma subseteq_intersection_2 X Y : X ∩ Y ≡ X → X ⊆ Y.
diff --git a/theories/tactics.v b/theories/tactics.v
index 00e7f9af..f9a13635 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -520,7 +520,7 @@ Ltac find_pat pat tac :=
       tryif tac x then idtac else fail 2
   end.
 
-(** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
+(** Coq's [firstorder] tactic fails or loops on rather small goals already. In
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
 to solve propositions on sets. The [naive_solver] tactic implements an
 ad-hoc and incomplete [firstorder]-like solver using Ltac's backtracking
-- 
GitLab