Delete trailing whitespaces in all *.{v,ml*} files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 146 insertions, 146 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 6ce34535e..4b9b26384 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -18,7 +18,7 @@
 
 Require Export Coq.Classes.Equivalence.
 
-(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
+(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more
    classically. *)
 
 Require Import Coq.Logic.Decidable.
@@ -43,8 +43,8 @@ Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70)
 
 Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
-    | left H => @right _ _ H 
-    | right H => @left _ _ H 
+    | left H => @right _ _ H
+    | right H => @left _ _ H
   end.
 
 Open Local Scope program_scope.
@@ -89,34 +89,34 @@ Obligation Tactic := unfold complement, equiv ; program_simpl.
 Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
   ! EqDec (prod A B) eq :=
   { equiv_dec x y :=
-    let '(x1, x2) := x in 
-    let '(y1, y2) := y in 
-    if x1 == y1 then 
+    let '(x1, x2) := x in
+    let '(y1, y2) := y in
+    if x1 == y1 then
       if x2 == y2 then in_left
       else in_right
     else in_right }.
 
 Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
   EqDec (sum A B) eq := {
-  equiv_dec x y := 
+  equiv_dec x y :=
     match x, y with
       | inl a, inl b => if a == b then in_left else in_right
       | inr a, inr b => if a == b then in_left else in_right
       | inl _, inr _ | inr _, inl _ => in_right
     end }.
 
-(** Objects of function spaces with countable domains like bool have decidable equality. 
+(** Objects of function spaces with countable domains like bool have decidable equality.
    Proving the reflection requires functional extensionality though. *)
 
 Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
-  { equiv_dec f g := 
+  { equiv_dec f g :=
     if f true == g true then
       if f false == g false then in_left
       else in_right
     else in_right }.
 
   Next Obligation.
-  Proof. 
+  Proof.
     extensionality x.
     destruct x ; auto.
   Qed.
@@ -124,11 +124,11 @@ Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
 Require Import List.
 
 Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
-  { equiv_dec := 
+  { equiv_dec :=
     fix aux (x : list A) y { struct x } :=
     match x, y with
       | nil, nil => in_left
-      | cons hd tl, cons hd' tl' => 
+      | cons hd tl, cons hd' tl' =>
         if hd == hd' then
           if aux tl tl' then in_left else in_right
           else in_right
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 100ddbe3e..aa20ebd49 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -7,10 +7,10 @@
 (************************************************************************)
 
 (* Typeclass-based setoids. Definitions on [Equivalence].
- 
+
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
-   91405 Orsay, France *) 
+   91405 Orsay, France *)
 
 (* $Id$ *)
 
@@ -34,7 +34,7 @@ Definition equiv `{Equivalence A R} : relation A := R.
 Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
 
 Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
-  
+
 Open Local Scope equiv_scope.
 
 (** Overloading for [PER]. *)
@@ -60,7 +60,7 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
 
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
-Ltac setoid_subst H := 
+Ltac setoid_subst H :=
   match type of H with
     ?x === ?y => substitute H ; clear H x
   end.
@@ -70,7 +70,7 @@ Ltac setoid_subst_nofail :=
     | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
     | _ => idtac
   end.
-  
+
 (** [subst*] will try its best at substituting every equality in the goal. *)
 
 Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
@@ -100,19 +100,19 @@ Ltac equivify := repeat equivify_tac.
 
 Section Respecting.
 
-  (** Here we build an equivalence instance for functions which relates respectful ones only, 
+  (** Here we build an equivalence instance for functions which relates respectful ones only,
      we do not export it. *)
 
-  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type := 
+  Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type :=
     { morph : A -> B | respectful R R' morph morph }.
-  
+
   Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
     Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
-  
+
   Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
 
   Next Obligation.
-  Proof. 
+  Proof.
     unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity.
   Qed.
 
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index b92e4d174..80d60d658 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (* Functional morphisms.
- 
+
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v
index 3e2eb4f40..7be92139e 100644
--- a/theories/Classes/Init.v
+++ b/theories/Classes/Init.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Initialization code for typeclasses, setting up the default tactic 
+(* Initialization code for typeclasses, setting up the default tactic
    for instance search.
 
    Author: Matthieu Sozeau
@@ -25,7 +25,7 @@ Typeclasses Opaque id const flip compose arrow impl iff not all.
 
 Ltac class_apply c := autoapply c using typeclass_instances.
 
-(** The unconvertible typeclass, to test that two objects of the same type are 
+(** The unconvertible typeclass, to test that two objects of the same type are
    actually different. *)
 
 Class Unconvertible (A : Type) (a b : A) := unconvertible : unit.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 595ad1297..55aad6e73 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -8,7 +8,7 @@
 (************************************************************************)
 
 (* Typeclass-based morphism definition and standard, minimal instances.
- 
+
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
@@ -22,11 +22,11 @@ Require Export Coq.Classes.RelationClasses.
 
 (** * Morphisms.
 
-   We now turn to the definition of [Proper] and declare standard instances. 
+   We now turn to the definition of [Proper] and declare standard instances.
    These will be used by the [setoid_rewrite] tactic later. *)
 
 (** A morphism for a relation [R] is a proper element of the relation.
-   The relation [R] will be instantiated by [respectful] and [A] by an arrow type 
+   The relation [R] will be instantiated by [respectful] and [A] by an arrow type
    for usual morphisms. *)
 
 Class Proper {A} (R : relation A) (m : A) : Prop :=
@@ -36,12 +36,12 @@ Class Proper {A} (R : relation A) (m : A) : Prop :=
 
 (** The fully dependent version, not used yet. *)
 
-Definition respectful_hetero 
-  (A B : Type) 
-  (C : A -> Type) (D : B -> Type) 
-  (R : A -> B -> Prop) 
-  (R' : forall (x : A) (y : B), C x -> D y -> Prop) : 
-    (forall x : A, C x) -> (forall x : B, D x) -> Prop := 
+Definition respectful_hetero
+  (A B : Type)
+  (C : A -> Type) (D : B -> Type)
+  (R : A -> B -> Prop)
+  (R' : forall (x : A) (y : B), C x -> D y -> Prop) :
+    (forall x : A, C x) -> (forall x : B, D x) -> Prop :=
     fun f g => forall x y, R x y -> R' x y (f x) (g y).
 
 (** The non-dependent version is an instance where we forget dependencies. *)
@@ -59,12 +59,12 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Module ProperNotations.
 
-  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) 
+  Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
     (right associativity, at level 55) : signature_scope.
-  
+
   Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
     (right associativity, at level 55) : signature_scope.
-  
+
   Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
     (right associativity, at level 55) : signature_scope.
 
@@ -74,7 +74,7 @@ Export ProperNotations.
 
 Open Local Scope signature_scope.
 
-(** Dependent pointwise lifting of a relation on the range. *) 
+(** Dependent pointwise lifting of a relation on the range. *)
 
 Definition forall_relation {A : Type} {B : A -> Type} (sig : Π a : A, relation (B a)) : relation (Π x : A, B x) :=
   λ f g, Π a : A, sig a (f a) (g a).
@@ -83,10 +83,10 @@ Arguments Scope forall_relation [type_scope type_scope signature_scope].
 
 (** Non-dependent pointwise lifting *)
 
-Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := 
+Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) :=
   Eval compute in forall_relation (B:=λ _, B) (λ _, R).
 
-Lemma pointwise_pointwise A B (R : relation B) : 
+Lemma pointwise_pointwise A B (R : relation B) :
   relation_equivalence (pointwise_relation A R) (@eq A ==> R).
 Proof. intros. split. simpl_relation. firstorder. Qed.
 
@@ -124,7 +124,7 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 Lemma subrelation_refl A R : @subrelation A R R.
 Proof. simpl_relation. Qed.
 
-Ltac subrelation_tac T U := 
+Ltac subrelation_tac T U :=
   (is_ground T ; is_ground U ; class_apply @subrelation_refl) ||
     class_apply @subrelation_respectful || class_apply @subrelation_refl.
 
@@ -141,13 +141,13 @@ Qed.
 CoInductive apply_subrelation : Prop := do_subrelation.
 
 Ltac proper_subrelation :=
-  match goal with 
+  match goal with
     [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper
   end.
 
 Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances.
 
-Instance proper_subrelation_proper : 
+Instance proper_subrelation_proper :
   Proper (subrelation ++> @eq _ ==> impl) (@Proper A).
 Proof. reduce. subst. firstorder. Qed.
 
@@ -176,7 +176,7 @@ Program Instance complement_proper
     intuition.
   Qed.
 
-(** The [inverse] too, actually the [flip] instance is a bit more general. *) 
+(** The [inverse] too, actually the [flip] instance is a bit more general. *)
 
 Program Instance flip_proper
   `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) :
@@ -187,7 +187,7 @@ Program Instance flip_proper
     apply mor ; auto.
   Qed.
 
-(** Every Transitive relation gives rise to a binary morphism on [impl], 
+(** Every Transitive relation gives rise to a binary morphism on [impl],
    contravariant in the first argument, covariant in the second. *)
 
 Program Instance trans_contra_co_morphism
@@ -263,13 +263,13 @@ Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1.
   Proof with auto.
     split ; intros.
     transitivity x0... transitivity x... symmetry...
-  
+
     transitivity y... transitivity y0... symmetry...
   Qed.
 
 Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R).
 Proof. firstorder. Qed.
-  
+
 Program Instance compose_proper A B C R₀ R₁ R₂ :
   Proper ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C).
 
@@ -279,7 +279,7 @@ Program Instance compose_proper A B C R₀ R₁ R₂ :
     unfold compose. apply H. apply H0. apply H1.
   Qed.
 
-(** Coq functions are morphisms for leibniz equality, 
+(** Coq functions are morphisms for leibniz equality,
    applied only if really needed. *)
 
 Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') :
@@ -288,13 +288,13 @@ Proof. simpl_relation. Qed.
 
 (** [respectful] is a morphism for relation equivalence. *)
 
-Instance respectful_morphism : 
+Instance respectful_morphism :
   Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B).
 Proof.
   reduce.
   unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *.
   split ; intros.
-  
+
     rewrite <- H0.
     apply H1.
     rewrite H.
@@ -308,10 +308,10 @@ Qed.
 
 (** Every element in the carrier of a reflexive relation is a morphism for this relation.
    We use a proxy class for this case which is used internally to discharge reflexivity constraints.
-   The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of 
+   The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of
    [Proper (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able
    to set different priorities in different hint bases and select a particular hint database for
-   resolution of a type class constraint.*) 
+   resolution of a type class constraint.*)
 
 Class ProperProxy {A} (R : relation A) (m : A) : Prop :=
   proper_proxy : R m m.
@@ -340,7 +340,7 @@ Class PartialApplication.
 
 CoInductive normalization_done : Prop := did_normalization.
 
-Ltac partial_application_tactic := 
+Ltac partial_application_tactic :=
   let rec do_partial_apps H m :=
     match m with
       | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H]
@@ -350,7 +350,7 @@ Ltac partial_application_tactic :=
   let rec do_partial H ar m :=
     match ar with
       | 0 => do_partial_apps H m
-      | S ?n' => 
+      | S ?n' =>
         match m with
           ?m' ?x => do_partial H n' m'
         end
@@ -362,18 +362,18 @@ Ltac partial_application_tactic :=
     let v := eval compute in n in clear n ;
     let H := fresh in
       assert(H:Params m' v) by typeclasses eauto ;
-      let v' := eval compute in v in 
+      let v' := eval compute in v in
       do_partial H v' m
  in
   match goal with
     | [ _ : normalization_done |- _ ] => fail 1
     | [ _ : @Params _ _ _ |- _ ] => fail 1
-    | [ |- @Proper ?T _ (?m ?x) ] => 
-      match goal with 
-        | [ _ : PartialApplication |- _ ] => 
+    | [ |- @Proper ?T _ (?m ?x) ] =>
+      match goal with
+        | [ _ : PartialApplication |- _ ] =>
           class_apply @Reflexive_partial_app_morphism
-        | _ => 
-          on_morphism (m x) || 
+        | _ =>
+          on_morphism (m x) ||
             (class_apply @Reflexive_partial_app_morphism ;
               [ pose Build_PartialApplication | idtac ])
       end
@@ -391,7 +391,7 @@ Qed.
 
 (** Special-purpose class to do normalization of signatures w.r.t. inverse. *)
 
-Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop := 
+Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop :=
   normalizes : relation_equivalence m m'.
 
 (** Current strategy: add [inverse] everywhere and reduce using [subrelation]
@@ -408,7 +408,7 @@ Proof. unfold Normalizes. intros.
   rewrite NA, NB. firstorder.
 Qed.
 
-Ltac inverse :=   
+Ltac inverse :=
   match goal with
     | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @inverse_arrow
     | _ => class_apply @inverse_atom
@@ -416,7 +416,7 @@ Ltac inverse :=
 
 Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances.
 
-(** Treating inverse: can't make them direct instances as we 
+(** Treating inverse: can't make them direct instances as we
    need at least a [flip] present in the goal. *)
 
 Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R.
@@ -477,7 +477,7 @@ Lemma reflexive_proper `{Reflexive A R} (x : A)
    : Proper R x.
 Proof. firstorder. Qed.
 
-Lemma proper_eq A (x : A) : Proper (@eq A) x. 
+Lemma proper_eq A (x : A) : Proper (@eq A) x.
 Proof. intros. apply reflexive_proper. Qed.
 
 Ltac proper_reflexive :=
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index b672651b9..5b61e2c07 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (* [Proper] instances for propositional connectives.
- 
+
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - Université Paris Sud
    91405 Orsay, France *)
@@ -25,7 +25,7 @@ Obligation Tactic := simpl_relation.
 Program Instance not_impl_morphism :
   Proper (impl --> impl) not | 1.
 
-Program Instance not_iff_morphism : 
+Program Instance not_iff_morphism :
   Proper (iff ++> iff) not.
 
 (** Logical conjunction. *)
@@ -33,15 +33,15 @@ Program Instance not_iff_morphism :
 Program Instance and_impl_morphism :
   Proper (impl ==> impl ==> impl) and | 1.
 
-Program Instance and_iff_morphism : 
+Program Instance and_iff_morphism :
   Proper (iff ==> iff ==> iff) and.
 
 (** Logical disjunction. *)
 
-Program Instance or_impl_morphism : 
+Program Instance or_impl_morphism :
   Proper (impl ==> impl ==> impl) or | 1.
 
-Program Instance or_iff_morphism : 
+Program Instance or_iff_morphism :
   Proper (iff ==> iff ==> iff) or.
 
 (** Logical implication [impl] is a morphism for logical equivalence. *)
@@ -54,11 +54,11 @@ Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff =
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.     
+    unfold pointwise_relation in H.
     split ; intros.
     destruct H0 as [x₁ H₁].
     exists x₁. rewrite H in H₁. assumption.
-    
+
     destruct H0 as [x₁ H₁].
     exists x₁. rewrite H. assumption.
   Qed.
@@ -68,20 +68,20 @@ Program Instance ex_impl_morphism {A : Type} :
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.  
+    unfold pointwise_relation in H.
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance ex_inverse_impl_morphism {A : Type} : 
+Program Instance ex_inverse_impl_morphism {A : Type} :
   Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A) | 1.
 
   Next Obligation.
   Proof.
-    unfold pointwise_relation in H.  
+    unfold pointwise_relation in H.
     exists H0. apply H. assumption.
   Qed.
 
-Program Instance all_iff_morphism {A : Type} : 
+Program Instance all_iff_morphism {A : Type} :
   Proper (pointwise_relation A iff ==> iff) (@all A).
 
   Next Obligation.
@@ -90,18 +90,18 @@ Program Instance all_iff_morphism {A : Type} :
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance all_impl_morphism {A : Type} : 
+Program Instance all_impl_morphism {A : Type} :
   Proper (pointwise_relation A impl ==> impl) (@all A) | 1.
-  
+
   Next Obligation.
   Proof.
     unfold pointwise_relation, all in *.
     intuition ; specialize (H x0) ; intuition.
   Qed.
 
-Program Instance all_inverse_impl_morphism {A : Type} : 
+Program Instance all_inverse_impl_morphism {A : Type} :
   Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1.
-  
+
   Next Obligation.
   Proof.
     unfold pointwise_relation, all in *.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index b603a2e41..e9301298e 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (* Morphism instances for relations.
- 
+
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
@@ -50,6 +50,6 @@ Instance subrelation_pointwise :
 Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed.
 
 
-Lemma inverse_pointwise_relation A (R : relation A) : 
+Lemma inverse_pointwise_relation A (R : relation A) :
   relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)).
 Proof. intros. split; firstorder. Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 5c6524481..b2f62cb87 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -8,7 +8,7 @@
 
 (* Typeclass-based relations, tactics and standard instances.
    This is the basic theory needed to formalize morphisms and setoids.
- 
+
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
    91405 Orsay, France *)
@@ -42,18 +42,18 @@ Unset Strict Implicit.
 Class Reflexive {A} (R : relation A) :=
   reflexivity : forall x, R x x.
 
-Class Irreflexive {A} (R : relation A) := 
+Class Irreflexive {A} (R : relation A) :=
   irreflexivity : Reflexive (complement R).
 
 Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclasses_instances.
 
-Class Symmetric {A} (R : relation A) := 
+Class Symmetric {A} (R : relation A) :=
   symmetry : forall x y, R x y -> R y x.
 
-Class Asymmetric {A} (R : relation A) := 
+Class Asymmetric {A} (R : relation A) :=
   asymmetry : forall x y, R x y -> R y x -> False.
 
-Class Transitive {A} (R : relation A) := 
+Class Transitive {A} (R : relation A) :=
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
 Hint Resolve @irreflexivity : ord.
@@ -63,7 +63,7 @@ Unset Implicit Arguments.
 (** A HintDb for relations. *)
 
 Ltac solve_relation :=
-  match goal with 
+  match goal with
   | [ |- ?R ?x ?x ] => reflexivity
   | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
   end.
@@ -85,7 +85,7 @@ Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) :=
 
 Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) :=
   fun x y H H' => asymmetry (R:=R) H H'.
-  
+
 Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) :=
   fun x y z H H' => transitivity (R:=R) H' H.
 
@@ -122,7 +122,7 @@ Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
 
 Ltac reduce := reduce_goal.
 
-Tactic Notation "apply" "*" constr(t) := 
+Tactic Notation "apply" "*" constr(t) :=
   first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
     refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
 
@@ -186,7 +186,7 @@ Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) :
 Proof. firstorder. Qed.
 
 (** Leibinz equality [eq] is an equivalence relation.
-   The instance has low priority as it is always applicable 
+   The instance has low priority as it is always applicable
    if only the type is constrained. *)
 
 Program Instance eq_equivalence : Equivalence (@eq A) | 10.
@@ -208,8 +208,8 @@ Require Import Coq.Lists.List.
 
 (** A compact representation of non-dependent arities, with the codomain singled-out. *)
 
-Fixpoint arrows (l : list Type) (r : Type) : Type := 
-  match l with 
+Fixpoint arrows (l : list Type) (r : Type) : Type :=
+  match l with
     | nil => r
     | A :: l' => A -> arrows l' r
   end.
@@ -232,7 +232,7 @@ Definition unary_predicate A := predicate (cons A nil).
 
 Definition binary_relation A := predicate (cons A (cons A nil)).
 
-(** We can close a predicate by universal or existential quantification. *) 
+(** We can close a predicate by universal or existential quantification. *)
 
 Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
   match l with
@@ -246,7 +246,7 @@ Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
     | A :: tl => fun f => exists x : A, predicate_exists tl (f x)
   end.
 
-(** Pointwise extension of a binary operation on [T] to a binary operation 
+(** Pointwise extension of a binary operation on [T] to a binary operation
    on functions whose codomain is [T].
    For an operator on [Prop] this lifts the operator to a binary operation. *)
 
@@ -254,7 +254,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
   (l : list Type) : binary_operation (arrows l T) :=
   match l with
     | nil => fun R R' => op R R'
-    | A :: tl => fun R R' => 
+    | A :: tl => fun R R' =>
       fun x => pointwise_extension op tl (R x) (R' x)
   end.
 
@@ -263,7 +263,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
 Fixpoint pointwise_lifting (op : binary_relation Prop)  (l : list Type) : binary_relation (predicate l) :=
   match l with
     | nil => fun R R' => op R R'
-    | A :: tl => fun R R' => 
+    | A :: tl => fun R R' =>
       forall x, pointwise_lifting op tl (R x) (R' x)
   end.
 
@@ -295,7 +295,7 @@ Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_
 
 (** The always [True] and always [False] predicates. *)
 
-Fixpoint true_predicate {l : list Type} : predicate l := 
+Fixpoint true_predicate {l : list Type} : predicate l :=
   match l with
     | nil => True
     | A :: tl => fun _ => @true_predicate tl
@@ -313,7 +313,7 @@ Notation "∙⊄∙" := false_predicate : predicate_scope.
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
 Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
-  Next Obligation. 
+  Next Obligation.
     induction l ; firstorder.
   Qed.
   Next Obligation.
@@ -333,11 +333,11 @@ Program Instance predicate_implication_preorder :
   Qed.
   Next Obligation.
     induction l. firstorder.
-    unfold predicate_implication in *. simpl in *. 
+    unfold predicate_implication in *. simpl in *.
     intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
   Qed.
 
-(** We define the various operations which define the algebra on binary relations, 
+(** We define the various operations which define the algebra on binary relations,
    from the general ones. *)
 
 Definition relation_equivalence {A : Type} : relation (relation A) :=
@@ -365,20 +365,20 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
 
 (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
-   We give an equivalent definition, up-to an equivalence relation 
+   We give an equivalent definition, up-to an equivalence relation
    on the carrier. *)
 
 Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
-(** The equivalence proof is sufficient for proving that [R] must be a morphism 
+(** The equivalence proof is sufficient for proving that [R] must be a morphism
    for equivalence (see Morphisms).
    It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
 
 Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. 
-  pose proof partial_order_equivalence as poe. do 3 red in poe. 
+  reduce_goal.
+  pose proof partial_order_equivalence as poe. do 3 red in poe.
   apply <- poe. firstorder.
 Qed.
 
@@ -392,7 +392,7 @@ Program Instance subrelation_partial_order :
     unfold relation_equivalence in *. firstorder.
   Qed.
 
-Typeclasses Opaque arrows predicate_implication predicate_equivalence 
+Typeclasses Opaque arrows predicate_implication predicate_equivalence
   relation_equivalence pointwise_lifting.
 
 (** Rewrite relation on a given support: declares a relation as a rewrite
@@ -409,7 +409,7 @@ Instance: RewriteRelation impl.
 Instance: RewriteRelation iff.
 Instance: RewriteRelation (@relation_equivalence A).
 
-(** Any [Equivalence] declared in the context is automatically considered 
+(** Any [Equivalence] declared in the context is automatically considered
    a rewrite relation. *)
 
 Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
index 469b9eae6..ebc1d7be9 100644
--- a/theories/Classes/SetoidAxioms.v
+++ b/theories/Classes/SetoidAxioms.v
@@ -21,7 +21,7 @@ Unset Strict Implicit.
 
 Require Export Coq.Classes.SetoidClass.
 
-(* Application of the extensionality axiom to turn a goal on 
+(* Application of the extensionality axiom to turn a goal on
    Leibniz equality to a setoid equivalence (use with care!). *)
 
 Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 055f02f8b..6af4b5ffe 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (* Typeclass-based setoids, tactics and standard instances.
- 
+
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
    91405 Orsay, France *)
@@ -55,7 +55,7 @@ Existing Instance setoid_trans.
 (* Program Instance eq_setoid : Setoid A := *)
 (*   equiv := eq ; setoid_equiv := eq_equivalence. *)
 
-Program Instance iff_setoid : Setoid Prop := 
+Program Instance iff_setoid : Setoid Prop :=
   { equiv := iff ; setoid_equiv := iff_equivalence }.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
@@ -69,7 +69,7 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) :
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
-Ltac clsubst H := 
+Ltac clsubst H :=
   match type of H with
     ?x == ?y => substitute H ; clear H x
   end.
@@ -79,7 +79,7 @@ Ltac clsubst_nofail :=
     | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail
     | _ => idtac
   end.
-  
+
 (** [subst*] will try its best at substituting every equality in the goal. *)
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
@@ -94,7 +94,7 @@ Qed.
 
 Lemma equiv_nequiv_trans : forall `{Setoid A} (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
-  intros; intro. 
+  intros; intro.
   assert(y == x) by (symmetry ; auto).
   assert(y == z) by (transitivity x ; eauto).
   contradiction.
@@ -127,7 +127,7 @@ Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Proper (
 
 (** Partial setoids don't require reflexivity so we can build a partial setoid on the function space. *)
 
-Class PartialSetoid (A : Type) := 
+Class PartialSetoid (A : Type) :=
   { pequiv : relation A ; pequiv_prf :> PER pequiv }.
 
 (** Overloaded notation for partial setoid equivalence. *)
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index d68e3fd22..71d80c959 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -21,7 +21,7 @@ Unset Strict Implicit.
 
 Require Export Coq.Classes.SetoidClass.
 
-(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
+(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more
    classically. *)
 
 Require Import Coq.Logic.Decidable.
@@ -41,8 +41,8 @@ Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70)
 
 Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
-    | left H => @right _ _ H 
-    | right H => @left _ _ H 
+    | left H => @right _ _ H
+    | right H => @left _ _ H
   end.
 
 Require Import Coq.Program.Program.
@@ -96,9 +96,9 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
 
 Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) :=
   λ x y,
-    let '(x1, x2) := x in 
-    let '(y1, y2) := y in 
-    if x1 == y1 then 
+    let '(x1, x2) := x in
+    let '(y1, y2) := y in
+    if x1 == y1 then
       if x2 == y2 then in_left
       else in_right
     else in_right.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index f58f227e5..12356385c 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -24,8 +24,8 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 (** Default relation on a given support. Can be used by tactics
-   to find a sensible default relation on any carrier. Users can 
-   declare an [Instance def : DefaultRelation A RA] anywhere to 
+   to find a sensible default relation on any carrier. Users can
+   declare an [Instance def : DefaultRelation A RA] anywhere to
    declare default relations. *)
 
 Class DefaultRelation A (R : relation A).
@@ -60,80 +60,80 @@ Ltac setoidreplaceat H t occs :=
 Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
   setoidreplace (default_relation x y) idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "at" int_or_var_list(o) :=
   setoidreplaceat (default_relation x y) idtac o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "in" hyp(id) :=
   setoidreplacein (default_relation x y) id idtac.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
-  "in" hyp(id) 
+  "in" hyp(id)
   "at" int_or_var_list(o) :=
   setoidreplaceinat (default_relation x y) id idtac o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "by" tactic3(t) :=
   setoidreplace (default_relation x y) ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "at" int_or_var_list(o) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "at" int_or_var_list(o)
   "by" tactic3(t) :=
   setoidreplaceat (default_relation x y) ltac:t o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "in" hyp(id) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "in" hyp(id)
   "by" tactic3(t) :=
   setoidreplacein (default_relation x y) id ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "in" hyp(id) 
-  "at" int_or_var_list(o) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "in" hyp(id)
+  "at" int_or_var_list(o)
   "by" tactic3(t) :=
   setoidreplaceinat (default_relation x y) id ltac:t o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel) :=
   setoidreplace (rel x y) idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "at" int_or_var_list(o) :=
   setoidreplaceat (rel x y) idtac o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "using" "relation" constr(rel) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "using" "relation" constr(rel)
   "by" tactic3(t) :=
   setoidreplace (rel x y) ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "using" "relation" constr(rel) 
-  "at" int_or_var_list(o)  
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "using" "relation" constr(rel)
+  "at" int_or_var_list(o)
   "by" tactic3(t) :=
   setoidreplaceat (rel x y) ltac:t o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id) :=
   setoidreplacein (rel x y) id idtac.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
-  "in" hyp(id) 
+  "in" hyp(id)
   "at" int_or_var_list(o) :=
   setoidreplaceinat (rel x y) id idtac o.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id)
   "by" tactic3(t) :=
   setoidreplacein (rel x y) id ltac:t.
 
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "using" "relation" constr(rel) 
+Tactic Notation "setoid_replace" constr(x) "with" constr(y)
+  "using" "relation" constr(rel)
   "in" hyp(id)
-  "at" int_or_var_list(o)  
+  "at" int_or_var_list(o)
   "by" tactic3(t) :=
   setoidreplaceinat (rel x y) id ltac:t o.