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

6 files changed, 138 insertions, 138 deletions

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index 9335f4834..c54756881 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -8,7 +8,7 @@
 (* $Id$ *)
 
 (** Standard functions and combinators.
-   
+
    Proofs about them require functional extensionality and can be found in [Combinators].
 
    Author: Matthieu Sozeau
@@ -21,12 +21,12 @@ Implicit Arguments id [[A]].
 
 (** Function composition. *)
 
-Definition compose {A B C} (g : B -> C) (f : A -> B) := 
+Definition compose {A B C} (g : B -> C) (f : A -> B) :=
   fun x : A => g (f x).
 
 Hint Unfold compose.
 
-Notation " g ∘ f " := (compose g f)  
+Notation " g ∘ f " := (compose g f)
   (at level 40, left associativity) : program_scope.
 
 Open Local Scope program_scope.
diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v
index 33ad3b556..e12f57668 100644
--- a/theories/Program/Combinators.v
+++ b/theories/Program/Combinators.v
@@ -34,7 +34,7 @@ Proof.
   symmetry ; apply eta_expansion.
 Qed.
 
-Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D), 
+Lemma compose_assoc : forall A B C D (f : A -> B) (g : B -> C) (h : C -> D),
   h ∘ g ∘ f = h ∘ (g ∘ f).
 Proof.
   intros.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index f35dc7adc..381a0bae4 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -26,7 +26,7 @@ Notation "'refl'" := (@refl_equal _ _).
 
 (** Do something on an heterogeneous equality appearing in the context. *)
 
-Ltac on_JMeq tac := 
+Ltac on_JMeq tac :=
   match goal with
     | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H
   end.
@@ -44,17 +44,17 @@ Ltac simpl_JMeq := repeat simpl_one_JMeq.
 
 Ltac simpl_one_dep_JMeq :=
   on_JMeq
-  ltac:(fun H => let H' := fresh "H" in 
+  ltac:(fun H => let H' := fresh "H" in
     assert (H' := JMeq_eq H)).
 
 Require Import Eqdep.
 
-(** Simplify dependent equality using sigmas to equality of the second projections if possible. 
+(** Simplify dependent equality using sigmas to equality of the second projections if possible.
    Uses UIP. *)
 
 Ltac simpl_existT :=
   match goal with
-    [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => 
+    [ H : existT _ ?x _ = existT _ ?x _ |- _ ] =>
     let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H
   end.
 
@@ -64,15 +64,15 @@ Ltac simpl_existTs := repeat simpl_existT.
 
 Ltac elim_eq_rect :=
   match goal with
-    | [ |- ?t ] => 
+    | [ |- ?t ] =>
       match t with
-        | context [ @eq_rect _ _ _ _ _ ?p ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
+        | context [ @eq_rect _ _ _ _ _ ?p ] =>
+          let P := fresh "P" in
+            set (P := p); simpl in P ;
 	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
-        | context [ @eq_rect _ _ _ _ _ ?p _ ] => 
-          let P := fresh "P" in 
-            set (P := p); simpl in P ; 
+        | context [ @eq_rect _ _ _ _ _ ?p _ ] =>
+          let P := fresh "P" in
+            set (P := p); simpl in P ;
 	      ((case P ; clear P) || (clearbody P; rewrite (UIP_refl _ _ P); clear P))
       end
   end.
@@ -90,18 +90,18 @@ Ltac simpl_eq := simpl ; unfold eq_rec_r, eq_rec ; repeat (elim_eq_rect ; simpl)
 
 (** Try to abstract a proof of equality, if no proof of the same equality is present in the context. *)
 
-Ltac abstract_eq_hyp H' p := 
+Ltac abstract_eq_hyp H' p :=
   let ty := type of p in
   let tyred := eval simpl in ty in
-    match tyred with  
-      ?X = ?Y => 
-      match goal with 
+    match tyred with
+      ?X = ?Y =>
+      match goal with
         | [ H : X = Y |- _ ] => fail 1
         | _ => set (H':=p) ; try (change p with H') ; clearbody H' ; simpl in H'
       end
     end.
 
-(** Apply the tactic tac to proofs of equality appearing as coercion arguments. 
+(** Apply the tactic tac to proofs of equality appearing as coercion arguments.
    Just redefine this tactic (using [Ltac on_coerce_proof tac ::=]) to handle custom coercion operators.
    *)
 
@@ -109,7 +109,7 @@ Ltac on_coerce_proof tac T :=
   match T with
     | context [ eq_rect _ _ _ _ ?p ] => tac p
   end.
-  
+
 Ltac on_coerce_proof_gl tac :=
   match goal with
     [ |- ?T ] => on_coerce_proof tac T
@@ -120,17 +120,17 @@ Ltac on_coerce_proof_gl tac :=
 Ltac abstract_eq_proof := on_coerce_proof_gl ltac:(fun p => let H := fresh "eqH" in abstract_eq_hyp H p).
 
 Ltac abstract_eq_proofs := repeat abstract_eq_proof.
-  
-(** Factorize proofs, by using proof irrelevance so that two proofs of the same equality 
+
+(** Factorize proofs, by using proof irrelevance so that two proofs of the same equality
    in the goal become convertible. *)
 
 Ltac pi_eq_proof_hyp p :=
   let ty := type of p in
   let tyred := eval simpl in ty in
   match tyred with
-    ?X = ?Y => 
-    match goal with 
-      | [ H : X = Y |- _ ] => 
+    ?X = ?Y =>
+    match goal with
+      | [ H : X = Y |- _ ] =>
         match p with
           | H => fail 2
           | _ => rewrite (proof_irrelevance (X = Y) p H)
@@ -162,28 +162,28 @@ Ltac rewrite_refl_id := autorewrite with refl_id.
 Ltac clear_eq_ctx :=
   rewrite_refl_id ; clear_eq_proofs.
 
-(** Reapeated elimination of [eq_rect] applications. 
+(** Reapeated elimination of [eq_rect] applications.
    Abstracting equalities makes it run much faster than an naive implementation. *)
 
-Ltac simpl_eqs := 
+Ltac simpl_eqs :=
   repeat (elim_eq_rect ; simpl ; clear_eq_ctx).
 
 (** Clear unused reflexivity proofs. *)
 
-Ltac clear_refl_eq := 
+Ltac clear_refl_eq :=
   match goal with [ H : ?X = ?X |- _ ] => clear H end.
 Ltac clear_refl_eqs := repeat clear_refl_eq.
 
 (** Clear unused equality proofs. *)
 
-Ltac clear_eq := 
+Ltac clear_eq :=
   match goal with [ H : _ = _ |- _ ] => clear H end.
 Ltac clear_eqs := repeat clear_eq.
 
 (** Combine all the tactics to simplify goals containing coercions. *)
 
-Ltac simplify_eqs := 
-  simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ;  
+Ltac simplify_eqs :=
+  simpl ; simpl_eqs ; clear_eq_ctx ; clear_refl_eqs ;
     try subst ; simpl ; repeat simpl_uip ; rewrite_refl_id.
 
 (** A tactic that tries to remove trivial equality guards in induction hypotheses coming
@@ -219,7 +219,7 @@ Ltac simpl_IH_eq H :=
 
 Ltac simpl_IH_eqs H := repeat simpl_IH_eq H.
 
-Ltac do_simpl_IHs_eqs := 
+Ltac do_simpl_IHs_eqs :=
   match goal with
     | [ H : context [ @JMeq _ _ _ _ -> _ ] |- _ ] => progress (simpl_IH_eqs H)
     | [ H : context [ _ = _ -> _ ] |- _ ] => progress (simpl_IH_eqs H)
@@ -227,17 +227,17 @@ Ltac do_simpl_IHs_eqs :=
 
 Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs.
 
-(** We split substitution tactics in the two directions depending on which 
+(** We split substitution tactics in the two directions depending on which
    names we want to keep corresponding to the generalization performed by the
    [generalize_eqs] tactic. *)
 
 Ltac subst_left_no_fail :=
-  repeat (match goal with 
+  repeat (match goal with
             [ H : ?X = ?Y |- _ ] => subst X
           end).
 
 Ltac subst_right_no_fail :=
-  repeat (match goal with 
+  repeat (match goal with
             [ H : ?X = ?Y |- _ ] => subst Y
           end).
 
@@ -250,32 +250,32 @@ Ltac inject_right H :=
 Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
 Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
 
-Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; 
+Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ;
   simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
 
-Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ; 
+Ltac simpl_depind_l := subst_left_no_fail ; autoinjections_left ; try discriminates ;
   simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
 
-Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ; 
+Ltac simpl_depind_r := subst_right_no_fail ; autoinjections_right ; try discriminates ;
   simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
 
 (** Support for the [Equations] command.
-   These tactics implement the necessary machinery to solve goals produced by the 
-   [Equations] command relative to dependent pattern-matching. 
+   These tactics implement the necessary machinery to solve goals produced by the
+   [Equations] command relative to dependent pattern-matching.
    It is completely inspired from the "Eliminating Dependent Pattern-Matching" paper by
    Goguen, McBride and McKinna. *)
 
 
 (** The NoConfusionPackage class provides a method for making progress on proving a property
    [P] implied by an equality on an inductive type [I]. The type of [noConfusion] for a given
-   [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where 
+   [P] should be of the form [ Π Δ, (x y : I Δ) (x = y) -> NoConfusion P x y ], where
    [NoConfusion P x y] for constructor-headed [x] and [y] will give a formula ending in [P].
    This gives a general method for simplifying by discrimination or injectivity of constructors.
-   
+
    Some actual instances are defined later in the file using the more primitive [discriminate] and
    [injection] tactics on which we can always fall back.
    *)
-  
+
 Class NoConfusionPackage (I : Type) := { NoConfusion : Π P : Prop, Type ; noConfusion : Π P, NoConfusion P }.
 
 (** The [DependentEliminationPackage] provides the default dependent elimination principle to
@@ -287,13 +287,13 @@ Class DependentEliminationPackage (A : Type) :=
 
 (** A higher-order tactic to apply a registered eliminator. *)
 
-Ltac elim_tac tac p := 
+Ltac elim_tac tac p :=
   let ty := type of p in
   let eliminator := eval simpl in (elim (A:=ty)) in
     tac p eliminator.
 
-(** Specialization to do case analysis or induction. 
-   Note: the [equations] tactic tries [case] before [elim_case]: there is no need to register 
+(** Specialization to do case analysis or induction.
+   Note: the [equations] tactic tries [case] before [elim_case]: there is no need to register
    generated induction principles. *)
 
 Ltac elim_case p := elim_tac ltac:(fun p el => destruct p using el) p.
@@ -308,7 +308,7 @@ Class BelowPackage (A : Type) := {
 
 (** The [Recursor] class defines a recursor on a type, based on some definition of [Below]. *)
 
-Class Recursor (A : Type) (BP : BelowPackage A) := 
+Class Recursor (A : Type) (BP : BelowPackage A) :=
   { rec_type : A -> Type ; rec : Π (a : A), rec_type a }.
 
 (** Lemmas used by the simplifier, mainly rephrasings of [eq_rect], [eq_ind]. *)
@@ -332,7 +332,7 @@ Proof. intros. apply X. apply inj_pair2. exact H. Defined.
 Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P q),
   (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B).
 Proof. intros. injection H. intros ; auto. Defined.
-  
+
 Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p).
 Proof. intros. rewrite (UIP_refl A). assumption. Defined.
 
@@ -342,26 +342,26 @@ Ltac unfold_equations :=
   unfold solution_left, solution_right, deletion, simplification_heq,
     simplification_existT1, simplification_existT2, eq_rect_r, eq_rec, eq_ind.
 
-(** The tactic [simplify_equations] is to be used when a program generated using [Equations] 
-   is in the goal. It simplifies it as much as possible, possibly using [K] if needed. *) 
+(** The tactic [simplify_equations] is to be used when a program generated using [Equations]
+   is in the goal. It simplifies it as much as possible, possibly using [K] if needed. *)
 
-Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs). 
+Ltac simplify_equations := repeat (unfold_equations ; simplify_eqs).
 
-(** We will use the [block_induction] definition to separate the goal from the 
+(** We will use the [block_induction] definition to separate the goal from the
    equalities generated by the tactic. *)
 
 Definition block_dep_elim {A : Type} (a : A) := a.
 
-(** Using these we can make a simplifier that will perform the unification 
+(** Using these we can make a simplifier that will perform the unification
    steps needed to put the goal in normalised form (provided there are only
    constructor forms). Compare with the lemma 16 of the paper.
-   We don't have a [noCycle] procedure yet. *) 
+   We don't have a [noCycle] procedure yet. *)
 
 Ltac simplify_one_dep_elim_term c :=
   match c with
     | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _)
     | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _)
-    | eq (existT _ _ _) (existT _ _ _) -> _ => 
+    | eq (existT _ _ _) (existT _ _ _) -> _ =>
       refine (simplification_existT2 _ _ _ _ _ _ _) ||
         refine (simplification_existT1 _ _ _ _ _ _ _ _)
     | ?x = ?y -> _ => (* variables case *)
@@ -413,12 +413,12 @@ Definition inaccessible_pattern {A : Type} (t : A) := t.
 Notation "?( t )" := (inaccessible_pattern t).
 
 (** To handle sections, we need to separate the context in two parts:
-   variables introduced by the section and the rest. We introduce a dummy variable 
+   variables introduced by the section and the rest. We introduce a dummy variable
    between them to indicate that. *)
 
 CoInductive end_of_section := the_end_of_the_section.
 
-Ltac set_eos := let eos := fresh "eos" in 
+Ltac set_eos := let eos := fresh "eos" in
   assert (eos:=the_end_of_the_section).
 
 (** We have a specialized [reverse_local] tactic to reverse the goal until the begining of the
@@ -426,14 +426,14 @@ Ltac set_eos := let eos := fresh "eos" in
 
 Ltac reverse_local :=
   match goal with
-    | [ H : ?T |- _ ] => 
+    | [ H : ?T |- _ ] =>
       match T with
         | end_of_section => idtac | _ => revert H ; reverse_local end
     | _ => idtac
   end.
 
 (** Do as much as possible to apply a method, trying to get the arguments right.
-   !!Unsafe!! We use [auto] for the [_nocomp] variant of [Equations], in which case some 
+   !!Unsafe!! We use [auto] for the [_nocomp] variant of [Equations], in which case some
    non-dependent arguments of the method can remain after [apply]. *)
 
 Ltac simpl_intros m := ((apply m || refine m) ; auto) || (intro ; simpl_intros m).
@@ -453,7 +453,7 @@ Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_loca
 
 (** Solving a method call: we can solve it by splitting on an empty family member
    or we must refine the goal until the body can be applied. *)
-    
+
 Ltac solve_method rec :=
   match goal with
     | [ H := ?body : nat |- _ ] => subst H ; clear ; abstract (simplify_method idtac ; solve_empty body)
@@ -463,21 +463,21 @@ Ltac solve_method rec :=
 (** Impossible cases, by splitting on a given target. *)
 
 Ltac solve_split :=
-  match goal with 
+  match goal with
     | [ |- let split := ?x : nat in _ ] => clear ; abstract (intros _ ; solve_empty x)
   end.
 
 (** If defining recursive functions, the prototypes come first. *)
 
 Ltac intro_prototypes :=
-  match goal with 
+  match goal with
     | [ |- Π x : _, _ ] => intro ; intro_prototypes
     | _ => idtac
   end.
 
-Ltac introduce p := first [ 
-  match p with _ => (* Already there, generalize dependent hyps *) 
-    generalize dependent p ; intros p 
+Ltac introduce p := first [
+  match p with _ => (* Already there, generalize dependent hyps *)
+    generalize dependent p ; intros p
   end
   | intros until p | intros ].
 
@@ -489,7 +489,7 @@ Ltac dep_elimify := match goal with [ |- ?T ] => change (block_dep_elim T) end.
 Ltac un_dep_elimify := unfold block_dep_elim in *.
 
 Ltac case_last := dep_elimify ;
-  on_last_hyp ltac:(fun p => 
+  on_last_hyp ltac:(fun p =>
     let ty := type of p in
       match ty with
         | ?x = ?x => revert p ; refine (simplification_K _ x _ _)
@@ -497,28 +497,28 @@ Ltac case_last := dep_elimify ;
         | _ => simpl in p ; generalize_eqs p ; do_case p
       end).
 
-Ltac nonrec_equations := 
+Ltac nonrec_equations :=
   solve [solve_equations (case_last) (solve_method idtac)] || solve [ solve_split ]
     || fail "Unnexpected equations goal".
 
 Ltac recursive_equations :=
-  solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ] 
+  solve [solve_equations (case_last) (solve_method ltac:intro)] || solve [ solve_split ]
     || fail "Unnexpected recursive equations goal".
 
 (** The [equations] tactic is the toplevel tactic for solving goals generated
    by [Equations]. *)
 
 Ltac equations := set_eos ;
-  match goal with 
+  match goal with
     | [ |- Π x : _, _ ] => intro ; recursive_equations
     | _ => nonrec_equations
   end.
 
 (** The following tactics allow to do induction on an already instantiated inductive predicate
-   by first generalizing it and adding the proper equalities to the context, in a maner similar to 
+   by first generalizing it and adding the proper equalities to the context, in a maner similar to
    the BasicElim tactic of "Elimination with a motive" by Conor McBride. *)
 
-(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis 
+(** The [do_depind] higher-order tactic takes an induction tactic as argument and an hypothesis
    and starts a dependent induction using this tactic. *)
 
 Ltac do_depind tac H :=
@@ -532,36 +532,36 @@ Ltac do_depind' tac H :=
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
    By default, we don't try to generalize the hyp by its variable indices.  *)
 
-Tactic Notation "dependent" "destruction" ident(H) := 
+Tactic Notation "dependent" "destruction" ident(H) :=
   do_depind' ltac:(fun hyp => do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
+Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) :=
   do_depind' ltac:(fun hyp => destruct hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
-Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) := 
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) :=
   do_depind' ltac:(fun hyp => revert l ; do_case hyp) H.
 
-Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
   do_depind' ltac:(fun hyp => revert l ; destruct hyp using c) H.
 
-(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by 
+(** Then we have wrappers for usual calls to induction. One can customize the induction tactic by
    writting another wrapper calling do_depind. We suppose the hyp has to be generalized before
    calling [induction]. *)
 
-Tactic Notation "dependent" "induction" ident(H) := 
+Tactic Notation "dependent" "induction" ident(H) :=
   do_depind ltac:(fun hyp => do_ind hyp) H.
 
-Tactic Notation "dependent" "induction" ident(H) "using" constr(c) := 
+Tactic Notation "dependent" "induction" ident(H) "using" constr(c) :=
   do_depind ltac:(fun hyp => induction hyp using c) H.
 
 (** This tactic also generalizes the goal by the given variables before the induction. *)
 
-Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) := 
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) :=
   do_depind' ltac:(fun hyp => generalize l ; clear l ; do_ind hyp) H.
 
-Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) := 
+Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) "using" constr(c) :=
   do_depind' ltac:(fun hyp => generalize l ; clear l ; induction hyp using c) H.
 
 Ltac simplify_IH_hyps := repeat
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index 14dc47358..a6aa4d524 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -14,7 +14,7 @@ Require Import Coq.Program.Equality.
 
 Open Local Scope program_scope.
 
-(** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to 
+(** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to
    factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
 
 Ltac on_subset_proof_aux tac T :=
@@ -27,25 +27,25 @@ Ltac on_subset_proof tac :=
     [ |- ?T ] => on_subset_proof_aux tac T
   end.
 
-Ltac abstract_any_hyp H' p := 
+Ltac abstract_any_hyp H' p :=
   match type of p with
-    ?X => 
-    match goal with 
+    ?X =>
+    match goal with
       | [ H : X |- _ ] => fail 1
       | _ => set (H':=p) ; try (change p with H') ; clearbody H'
     end
   end.
 
-Ltac abstract_subset_proof := 
+Ltac abstract_subset_proof :=
   on_subset_proof ltac:(fun p => let H := fresh "eqH" in abstract_any_hyp H p ; simpl in H).
 
 Ltac abstract_subset_proofs := repeat abstract_subset_proof.
 
 Ltac pi_subset_proof_hyp p :=
   match type of p with
-    ?X => 
-    match goal with 
-      | [ H : X |- _ ] => 
+    ?X =>
+    match goal with
+      | [ H : X |- _ ] =>
         match p with
           | H => fail 2
           | _ => rewrite (proof_irrelevance X p H)
@@ -78,16 +78,16 @@ Proof.
   pi.
 Qed.
 
-(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] 
+(* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f]
    in tactics. *)
 
 Definition match_eq (A B : Type) (x : A) (fn : forall (y : A | y = x), B) : B :=
   fn (exist _ x (refl_equal x)).
 
-(* This is what we want to be able to do: replace the originaly matched object by a new, 
+(* This is what we want to be able to do: replace the originaly matched object by a new,
    propositionally equal one. If [fn] works on [x] it should work on any [y | y = x]. *)
 
-Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B) 
+Lemma match_eq_rewrite : forall (A B : Type) (x : A) (fn : forall (y : A | y = x), B)
   (y : A | y = x),
   match_eq A B x fn = fn y.
 Proof.
@@ -103,9 +103,9 @@ Qed.
 (** Now we make a tactic to be able to rewrite a term [t] which is applied to a [match_eq] using an arbitrary
    equality [t = u], and [u] is now the subject of the [match]. *)
 
-Ltac rewrite_match_eq H := 
+Ltac rewrite_match_eq H :=
   match goal with
-    [ |- ?T ] => 
+    [ |- ?T ] =>
     match T with
       context [ match_eq ?A ?B ?t ?f ] =>
       rewrite (match_eq_rewrite A B t f (exist _ _ (sym_eq H)))
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 7e8fedceb..881297955 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -15,13 +15,13 @@
 
 Ltac show_goal := match goal with [ |- ?T ] => idtac T end.
 
-Ltac show_hyp id := 
-  match goal with 
-    | [ H := ?b : ?T |- _ ] => 
+Ltac show_hyp id :=
+  match goal with
+    | [ H := ?b : ?T |- _ ] =>
       match H with
         | id => idtac id ":=" b ":" T
       end
-    | [ H : ?T |- _ ] => 
+    | [ H : ?T |- _ ] =>
       match H with
         | id => idtac id  ":"  T
       end
@@ -77,7 +77,7 @@ Ltac destruct_exists := repeat (destruct_one_ex).
 
 Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex).
 
-(** Destruct an existential hypothesis [t] keeping its name for the first component 
+(** Destruct an existential hypothesis [t] keeping its name for the first component
    and using [Ht] for the second *)
 
 Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht].
@@ -96,7 +96,7 @@ Ltac discriminates :=
 
 (** Revert the last hypothesis. *)
 
-Ltac revert_last := 
+Ltac revert_last :=
   match goal with
     [ H : _ |- _ ] => revert H
   end.
@@ -108,8 +108,8 @@ Ltac reverse := repeat revert_last.
 (** Clear duplicated hypotheses *)
 
 Ltac clear_dup :=
-  match goal with 
-    | [ H : ?X |- _ ] => 
+  match goal with
+    | [ H : ?X |- _ ] =>
       match goal with
         | [ H' : ?Y |- _ ] =>
           match H with
@@ -124,7 +124,7 @@ Ltac clear_dups := repeat clear_dup.
 (** A non-failing subst that substitutes as much as possible. *)
 
 Ltac subst_no_fail :=
-  repeat (match goal with 
+  repeat (match goal with
             [ H : ?X = ?Y |- _ ] => subst X || subst Y
           end).
 
@@ -139,13 +139,13 @@ Ltac on_application f tac T :=
     | context [f ?x ?y ?z ?w ?v] => tac (f x y z w v)
     | context [f ?x ?y ?z ?w] => tac (f x y z w)
     | context [f ?x ?y ?z] => tac (f x y z)
-    | context [f ?x ?y] => tac (f x y) 
+    | context [f ?x ?y] => tac (f x y)
     | context [f ?x] => tac (f x)
   end.
 
 (** A variant of [apply] using [refine], doing as much conversion as necessary. *)
 
-Ltac rapply p := 
+Ltac rapply p :=
   refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
   refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
   refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
@@ -162,7 +162,7 @@ Ltac rapply p :=
   refine (p _ _) ||
   refine (p _) ||
   refine p.
-  
+
 (** Tactical [on_call f tac] applies [tac] on any application of [f] in the hypothesis or goal. *)
 
 Ltac on_call f tac :=
@@ -195,15 +195,15 @@ Tactic Notation "destruct_call" constr(f) := destruct_call f.
 
 (** Permit to name the results of destructing the call to [f]. *)
 
-Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) := 
+Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) :=
   destruct_call_as f l.
 
 (** Specify the hypothesis in which the call occurs as well. *)
 
-Tactic Notation "destruct_call" constr(f) "in" hyp(id) := 
+Tactic Notation "destruct_call" constr(f) "in" hyp(id) :=
   destruct_call_in f id.
 
-Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) := 
+Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(id) :=
   destruct_call_as_in f l id.
 
 (** A marker for prototypes to destruct. *)
@@ -215,7 +215,7 @@ Ltac destruct_rec_calls :=
     | [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H
   end.
 
-Ltac destruct_all_rec_calls := 
+Ltac destruct_all_rec_calls :=
   repeat destruct_rec_calls ; unfold fix_proto in *.
 
 (** Try to inject any potential constructor equality hypothesis. *)
@@ -237,23 +237,23 @@ Ltac destruct_nondep H := let H0 := fresh "H" in assert(H0 := H); destruct H0.
 
 Ltac bang :=
   match goal with
-    | |- ?x => 
+    | |- ?x =>
       match x with
         | context [False_rect _ ?p] => elim p
       end
   end.
- 
+
 (** A tactic to show contradiction by first asserting an automatically provable hypothesis. *)
-Tactic Notation "contradiction" "by" constr(t) := 
+Tactic Notation "contradiction" "by" constr(t) :=
   let H := fresh in assert t as H by auto with * ; contradiction.
 
 (** A tactic that adds [H:=p:typeof(p)] to the context if no hypothesis of the same type appears in the goal.
    Useful to do saturation using tactics. *)
 
-Ltac add_hypothesis H' p := 
+Ltac add_hypothesis H' p :=
   match type of p with
-    ?X => 
-    match goal with 
+    ?X =>
+    match goal with
       | [ H : X |- _ ] => fail 1
       | _ => set (H':=p) ; try (change p with H') ; clearbody H'
     end
@@ -281,11 +281,11 @@ Ltac refine_hyp c :=
     end.
 
 (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto]
-   is not enough, better rebind using [Obligation Tactic := tac] in this case, 
+   is not enough, better rebind using [Obligation Tactic := tac] in this case,
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)
 
 Ltac program_simplify :=
-  simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in *); 
+  simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl proj1_sig in *);
   subst*; autoinjections ; try discriminates ;
     try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]).
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 041b318e8..9b7ea0474 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -22,20 +22,20 @@ Section Well_founded.
   Variable A : Type.
   Variable R : A -> A -> Prop.
   Hypothesis Rwf : well_founded R.
-    
+
   Variable P : A -> Type.
-  
+
   Variable F_sub : forall x:A, (forall y: { y : A | R y x }, P (proj1_sig y)) -> P x.
-  
+
   Fixpoint Fix_F_sub (x : A) (r : Acc R x) {struct r} : P x :=
-    F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y) 
+    F_sub x (fun y: { y : A | R y x}  => Fix_F_sub (proj1_sig y)
       (Acc_inv r (proj2_sig y))).
-  
+
   Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
-  
-  (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)  
+
+  (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)
   (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *)
-  
+
   Hypothesis
     F_ext :
     forall (x:A) (f g:forall y:{y:A | R y x}, P (`y)),
@@ -44,10 +44,10 @@ Section Well_founded.
   Lemma Fix_F_eq :
     forall (x:A) (r:Acc R x),
       F_sub x (fun (y:A|R y x) => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
-  Proof. 
+  Proof.
     destruct r using Acc_inv_dep; auto.
   Qed.
-  
+
   Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s.
   Proof.
     intro x; induction (Rwf x); intros.
@@ -115,7 +115,7 @@ Section Fix_rects.
   Variable R : A -> A -> Prop.
   Variable Rwf : well_founded R.
   Variable f: forall (x : A), (forall y: { y: A | R y x }, P (proj1_sig y)) -> P x.
-  
+
   Lemma F_unfold x r:
     Fix_F_sub A R P f x r =
     f (fun y => Fix_F_sub A R P f (proj1_sig y) (Acc_inv r (proj2_sig y))).
@@ -200,8 +200,8 @@ Section Fix_rects.
     intros.
     assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))...
     set (inv x0 X0 a). clearbody q.
-    rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => 
-      Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) 
+    rewrite <- (equiv_lowers (fun y: {y: A | R y x0} =>
+      Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y)))
     (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...
     intros.
     apply eq_Fix_F_sub.
@@ -213,9 +213,9 @@ End Fix_rects.
 
 Ltac fold_sub f :=
   match goal with
-    | [ |- ?T ] => 
+    | [ |- ?T ] =>
       match T with
-        appcontext C [ @Fix_sub _ _ _ _ ?arg ] => 
+        appcontext C [ @Fix_sub _ _ _ _ ?arg ] =>
         let app := context C [ f arg ] in
           change app
       end
@@ -230,7 +230,7 @@ Module WfExtensionality.
 
   (** The two following lemmas allow to unfold a well-founded fixpoint definition without
      restriction using the functional extensionality axiom. *)
-  
+
   (** For a function defined with Program using a well-founded order. *)
 
   Program Lemma fix_sub_eq_ext :
@@ -247,11 +247,11 @@ Module WfExtensionality.
     extensionality y ; apply H.
     rewrite H0 ; auto.
   Qed.
-  
+
   (** Tactic to unfold once a definition based on [Fix_sub]. *)
-  
-  Ltac unfold_sub f fargs := 
-    set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; 
+
+  Ltac unfold_sub f fargs :=
+    set (call:=fargs) ; unfold f in call ; unfold call ; clear call ;
       rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
 
 End WfExtensionality.