Updated PR by removing whitespaces. Bug 17450.

1 files changed, 44 insertions, 44 deletions

diff --git a/lib/FSetAVLplus.v b/lib/FSetAVLplus.v
index eab427be..f16805c6 100644
--- a/lib/FSetAVLplus.v
+++ b/lib/FSetAVLplus.v
@@ -65,7 +65,7 @@ Proof.
 - discriminate.
 - destruct (above_low_bound t1) eqn: LB; [destruct (below_high_bound t1) eqn: HB | idtac].
   + (* in interval *)
-    exists t1; split; auto.  apply Raw.IsRoot. auto. 
+    exists t1; split; auto.  apply Raw.IsRoot. auto.
   + (* above interval *)
     exploit IHm1; auto. intros [x' [A B]]. exists x'; split; auto. apply Raw.InLeft; auto.
   + (* below interval *)
@@ -80,7 +80,7 @@ Lemma raw_mem_between_2:
 Proof.
   induction 1; simpl; intros.
 - inv H.
-- rewrite Raw.In_node_iff in H1. 
+- rewrite Raw.In_node_iff in H1.
   destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac].
   + (* in interval *)
     auto.
@@ -98,7 +98,7 @@ Theorem mem_between_1:
   mem_between s = true ->
   exists x, In x s /\ above_low_bound x = true /\ below_high_bound x = true.
 Proof.
-  intros. apply raw_mem_between_1. auto. 
+  intros. apply raw_mem_between_1. auto.
 Qed.
 
 Theorem mem_between_2:
@@ -138,9 +138,9 @@ Remark In_raw_elements_between_1:
 Proof.
   induction m; simpl; intros.
 - inv H.
-- rewrite Raw.In_node_iff. 
+- rewrite Raw.In_node_iff.
   destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
-  + rewrite Raw.join_spec in H. intuition. 
+  + rewrite Raw.join_spec in H. intuition.
   + left; apply IHm1; auto.
   + right; right; apply IHm2; auto.
 Qed.
@@ -174,7 +174,7 @@ Proof.
 - inv H.
 - destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
   + rewrite Raw.join_spec in H. intuition.
-    apply above_monotone with t1; auto. 
+    apply above_monotone with t1; auto.
     apply below_monotone with t1; auto.
   + auto.
   + auto.
@@ -190,7 +190,7 @@ Proof.
 - auto.
 - rewrite Raw.In_node_iff in H1.
   destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac].
-  + rewrite Raw.join_spec. intuition. 
+  + rewrite Raw.join_spec. intuition.
   + assert (X.eq x x0 \/ X.lt x0 x -> False).
     { intros. exploit below_monotone; eauto. congruence. }
     intuition. elim H7. apply g. auto.
@@ -204,7 +204,7 @@ Theorem elements_between_iff:
   In x (elements_between s) <-> In x s /\ above_low_bound x = true /\ below_high_bound x = true.
 Proof.
   intros. unfold elements_between, In; simpl. split.
-  intros. split. apply In_raw_elements_between_1; auto. eapply In_raw_elements_between_2; eauto. 
+  intros. split. apply In_raw_elements_between_1; auto. eapply In_raw_elements_between_2; eauto.
   intros [A [B C]]. apply In_raw_elements_between_3; auto. apply MSet.is_ok.
 Qed.
 
@@ -254,24 +254,24 @@ Lemma raw_for_all_between_1:
   pred x = true.
 Proof.
   induction 1; simpl; intros.
-- inv H0. 
+- inv H0.
 - destruct (above_low_bound x0) eqn: LB; [destruct (below_high_bound x0) eqn: HB | idtac].
   + (* in interval *)
     destruct (andb_prop _ _ H1) as [P C]. destruct (andb_prop _ _ P) as [A B]. clear H1 P.
     inv H2.
-    * erewrite pred_compat; eauto. 
+    * erewrite pred_compat; eauto.
     * apply IHbst1; auto.
     * apply IHbst2; auto.
   + (* above interval *)
     inv H2.
-    * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). 
+    * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
       congruence.
     * apply IHbst1; auto.
     * assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
       congruence.
   + (* below interval *)
     inv H2.
-    * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). 
+    * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
       congruence.
     * assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
       congruence.
@@ -290,7 +290,7 @@ Proof.
   + (* in interval *)
     rewrite IHbst1. rewrite (H1 x). rewrite IHbst2. auto.
     intros. apply H1; auto. apply Raw.InRight; auto.
-    apply Raw.IsRoot. reflexivity. auto. auto. 
+    apply Raw.IsRoot. reflexivity. auto. auto.
     intros. apply H1; auto. apply Raw.InLeft; auto.
   + (* above interval *)
     apply IHbst1. intros. apply H1; auto. apply Raw.InLeft; auto.
@@ -303,7 +303,7 @@ Theorem for_all_between_iff:
   for_all_between s = true <-> (forall x, In x s -> above_low_bound x = true -> below_high_bound x = true -> pred x = true).
 Proof.
   unfold for_all_between; intros; split; intros.
-- eapply raw_for_all_between_1; eauto. apply MSet.is_ok. 
+- eapply raw_for_all_between_1; eauto. apply MSet.is_ok.
 - apply raw_for_all_between_2; auto. apply MSet.is_ok.
 Qed.
 
@@ -337,10 +337,10 @@ Remark In_raw_partition_between_1:
 Proof.
   induction m; simpl; intros.
 - inv H.
-- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *.
   destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
   destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
-  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition. 
+  + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
   + rewrite Raw.In_node_iff. intuition.
   + rewrite Raw.In_node_iff. intuition.
 Qed.
@@ -351,10 +351,10 @@ Remark In_raw_partition_between_2:
 Proof.
   induction m; simpl; intros.
 - inv H.
-- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *.
   destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
   destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
-  + rewrite Raw.concat_spec in H. rewrite Raw.In_node_iff. intuition. 
+  + rewrite Raw.concat_spec in H. rewrite Raw.In_node_iff. intuition.
   + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
   + rewrite Raw.join_spec in H. rewrite Raw.In_node_iff. intuition.
 Qed.
@@ -364,22 +364,22 @@ Lemma raw_partition_between_ok:
 Proof.
   induction 1; simpl.
 - split; constructor.
-- destruct IHbst1 as [L1 L2]. destruct IHbst2 as [R1 R2]. 
-  destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+- destruct IHbst1 as [L1 L2]. destruct IHbst2 as [R1 R2].
+  destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *.
   destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
   destruct (above_low_bound x) eqn:LB; [destruct (below_high_bound x) eqn: RB | idtac]; simpl.
   + split.
     apply Raw.join_ok; auto.
-    red; intros. apply l0. apply In_raw_partition_between_1. rewrite LEQ; auto. 
+    red; intros. apply l0. apply In_raw_partition_between_1. rewrite LEQ; auto.
     red; intros. apply g. apply In_raw_partition_between_1. rewrite REQ; auto.
     apply Raw.concat_ok; auto.
-    intros. transitivity x. 
-    apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. 
+    intros. transitivity x.
+    apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto.
     apply g. apply In_raw_partition_between_2. rewrite REQ; auto.
   + split.
     auto.
     apply Raw.join_ok; auto.
-    red; intros. apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto. 
+    red; intros. apply l0. apply In_raw_partition_between_2. rewrite LEQ; auto.
   + split.
     auto.
     apply Raw.join_ok; auto.
@@ -397,11 +397,11 @@ Remark In_raw_partition_between_3:
 Proof.
   induction m; simpl; intros.
 - inv H.
-- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *. 
+- destruct (raw_partition_between m1) as [l1 l2] eqn:LEQ; simpl in *.
   destruct (raw_partition_between m2) as [r1 r2] eqn:REQ; simpl in *.
   destruct (above_low_bound t1) eqn:LB; [destruct (below_high_bound t1) eqn: RB | idtac]; simpl in H.
   + rewrite Raw.join_spec in H. intuition.
-    apply above_monotone with t1; auto. 
+    apply above_monotone with t1; auto.
     apply below_monotone with t1; auto.
   + auto.
   + auto.
@@ -414,17 +414,17 @@ Remark In_raw_partition_between_4:
 Proof.
   induction 1; simpl; intros.
 - inv H.
-- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *.
   destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
   destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
-  + simpl in H1. rewrite Raw.concat_spec in H1. intuition. 
+  + simpl in H1. rewrite Raw.concat_spec in H1. intuition.
   + assert (forall y, X.eq y x0 \/ X.lt x0 y -> below_high_bound y = false).
-    { intros. destruct (below_high_bound y) eqn:E; auto. 
+    { intros. destruct (below_high_bound y) eqn:E; auto.
       assert (below_high_bound x0 = true) by (apply below_monotone with y; auto).
       congruence. }
     simpl in H1. rewrite Raw.join_spec in H1. intuition.
   + assert (forall y, X.eq y x0 \/ X.lt y x0 -> above_low_bound y = false).
-    { intros. destruct (above_low_bound y) eqn:E; auto. 
+    { intros. destruct (above_low_bound y) eqn:E; auto.
       assert (above_low_bound x0 = true) by (apply above_monotone with y; auto).
       congruence. }
     simpl in H1. rewrite Raw.join_spec in H1. intuition.
@@ -438,23 +438,23 @@ Remark In_raw_partition_between_5:
 Proof.
   induction 1; simpl; intros.
 - inv H.
-- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *.
   destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
   destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
-  + simpl. rewrite Raw.join_spec. inv H1. 
+  + simpl. rewrite Raw.join_spec. inv H1.
     auto.
-    right; left; apply IHbst1; auto. 
+    right; left; apply IHbst1; auto.
     right; right; apply IHbst2; auto.
-  + simpl. inv H1. 
+  + simpl. inv H1.
     assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
     congruence.
-    auto. 
-    assert (below_high_bound x0 = true) by (apply below_monotone with x; auto). 
+    auto.
+    assert (below_high_bound x0 = true) by (apply below_monotone with x; auto).
     congruence.
-  + simpl. inv H1. 
+  + simpl. inv H1.
     assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
     congruence.
-    assert (above_low_bound x0 = true) by (apply above_monotone with x; auto). 
+    assert (above_low_bound x0 = true) by (apply above_monotone with x; auto).
     congruence.
     eauto.
 Qed.
@@ -467,7 +467,7 @@ Remark In_raw_partition_between_6:
 Proof.
   induction 1; simpl; intros.
 - inv H.
-- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *. 
+- destruct (raw_partition_between l) as [l1 l2] eqn:LEQ; simpl in *.
   destruct (raw_partition_between r) as [r1 r2] eqn:REQ; simpl in *.
   destruct (above_low_bound x0) eqn:LB; [destruct (below_high_bound x0) eqn: RB | idtac]; simpl in H.
   + simpl. rewrite Raw.concat_spec. inv H1.
@@ -476,11 +476,11 @@ Proof.
     destruct H2; congruence.
     left; apply IHbst1; auto.
     right; apply IHbst2; auto.
-  + simpl. rewrite Raw.join_spec. inv H1. 
+  + simpl. rewrite Raw.join_spec. inv H1.
     auto.
-    right; left; apply IHbst1; auto. 
+    right; left; apply IHbst1; auto.
     auto.
-  + simpl. rewrite Raw.join_spec. inv H1. 
+  + simpl. rewrite Raw.join_spec. inv H1.
     auto.
     auto.
     right; right; apply IHbst2; auto.
@@ -496,7 +496,7 @@ Theorem partition_between_iff_1:
   In x (fst (partition_between s)) <->
   In x s /\ above_low_bound x = true /\ below_high_bound x = true.
 Proof.
-  intros. unfold partition_between, In; simpl. split. 
+  intros. unfold partition_between, In; simpl. split.
   intros. split. apply In_raw_partition_between_1; auto. eapply In_raw_partition_between_3; eauto.
   intros [A [B C]]. apply In_raw_partition_between_5; auto. apply MSet.is_ok.
 Qed.
@@ -506,7 +506,7 @@ Theorem partition_between_iff_2:
   In x (snd (partition_between s)) <->
   In x s /\ (above_low_bound x = false \/ below_high_bound x = false).
 Proof.
-  intros. unfold partition_between, In; simpl. split. 
+  intros. unfold partition_between, In; simpl. split.
   intros. split. apply In_raw_partition_between_2; auto. eapply In_raw_partition_between_4; eauto. apply MSet.is_ok.
   intros [A B]. apply In_raw_partition_between_6; auto. apply MSet.is_ok.
 Qed.