1 files changed, 77 insertions, 77 deletions

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