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

5 files changed, 233 insertions, 233 deletions

diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index cd0f1afe9..36da9463b 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -15,7 +15,7 @@ Unset Boxed Definitions.
 
 Open Scope positive_scope.
 
-Ltac clean := try (simpl; congruence). 
+Ltac clean := try (simpl; congruence).
 Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t.
 
 Functional Scheme Pcompare_ind := Induction for Pcompare Sort Prop.
@@ -85,7 +85,7 @@ match m, n with
 | xO mm, xO nn => pos_eq mm nn
 | xH, xH => true
 | _, _ => false
-end. 
+end.
 
 Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
 induction m;simpl;intro n;destruct n;congruence ||
@@ -120,12 +120,12 @@ Theorem pos_eq_dec_ex : forall m n,
 fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence).
 simpl;intro e.
 elim (pos_eq_dec_ex _ _ e).
-intros x ex; rewrite ex. 
+intros x ex; rewrite ex.
 exists (f_equal xI x).
 reflexivity.
 simpl;intro e.
 elim (pos_eq_dec_ex _ _ e).
-intros x ex; rewrite ex. 
+intros x ex; rewrite ex.
 exists (f_equal xO x).
 reflexivity.
 simpl.
@@ -134,7 +134,7 @@ reflexivity.
 Qed.
 
 Fixpoint nat_eq (m n:nat) {struct m}: bool:=
-match m, n with 
+match m, n with
 O,O => true
 | S mm,S nn => nat_eq mm nn
 | _,_ => false
@@ -151,14 +151,14 @@ Defined.
 
 Fixpoint Lget (A:Set) (n:nat) (l:list A) {struct l}:option A :=
 match l with nil => None
-| x::q => 
+| x::q =>
 match n with O => Some x
 | S m => Lget A m q
 end end .
 
 Implicit Arguments Lget [A].
 
-Lemma map_app : forall (A B:Set) (f:A -> B) l m, 
+Lemma map_app : forall (A B:Set) (f:A -> B) l m,
 List.map  f (l ++ m) = List.map  f  l ++ List.map  f  m.
 induction l.
 reflexivity.
@@ -166,16 +166,16 @@ simpl.
 intro m ; apply f_equal with (list B);apply IHl.
 Qed.
 
-Lemma length_map : forall (A B:Set) (f:A -> B) l, 
+Lemma length_map : forall (A B:Set) (f:A -> B) l,
 length (List.map  f l) = length l.
 induction l.
 reflexivity.
 simpl; apply f_equal with nat;apply IHl.
 Qed.
 
-Lemma Lget_map : forall (A B:Set) (f:A -> B) i l, 
-Lget i (List.map  f l) = 
-match Lget i l with Some a => 
+Lemma Lget_map : forall (A B:Set) (f:A -> B) i l,
+Lget i (List.map  f l) =
+match Lget i l with Some a =>
 Some (f a) | None => None end.
 induction i;intros [ | x l ] ;trivial.
 simpl;auto.
@@ -190,7 +190,7 @@ reflexivity.
 auto.
 Qed.
 
-Lemma Lget_app_Some : forall (A:Set) l delta i (a: A), 
+Lemma Lget_app_Some : forall (A:Set) l delta i (a: A),
 Lget i l = Some a ->
 Lget i (l ++ delta) = Some a.
 induction l;destruct i;simpl;try congruence;auto.
@@ -208,8 +208,8 @@ Inductive Tree : Type :=
    Tempty : Tree
  | Branch0 : Tree -> Tree -> Tree
  | Branch1 : A -> Tree -> Tree -> Tree.
-        
-Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption := 
+
+Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption :=
   match T with
     Tempty => PNone
   | Branch0 T1 T2 =>
@@ -226,7 +226,7 @@ Fixpoint Tget (p:positive) (T:Tree) {struct p} : Poption :=
     end
 end.
 
-Fixpoint Tadd (p:positive) (a:A) (T:Tree) {struct p}: Tree := 
+Fixpoint Tadd (p:positive) (a:A) (T:Tree) {struct p}: Tree :=
  match T with
    | Tempty =>
        match p with
@@ -253,13 +253,13 @@ Definition mkBranch0 (T1 T2:Tree) :=
     Tempty ,Tempty => Tempty
   | _,_ => Branch0 T1 T2
   end.
-  
+
 Fixpoint Tremove (p:positive) (T:Tree) {struct p}: Tree :=
    match T with
       | Tempty => Tempty
-      | Branch0 T1 T2 => 
+      | Branch0 T1 T2 =>
         match p with
-        | xI pp => mkBranch0 T1 (Tremove pp T2)                  
+        | xI pp => mkBranch0 T1 (Tremove pp T2)
         | xO pp => mkBranch0 (Tremove pp T1) T2
         | xH => T
         end
@@ -270,8 +270,8 @@ Fixpoint Tremove (p:positive) (T:Tree) {struct p}: Tree :=
         | xH => mkBranch0 T1 T2
         end
       end.
-                                                                                                                        
- 
+
+
 Theorem Tget_Tempty: forall (p : positive), Tget p (Tempty) = PNone.
 destruct p;reflexivity.
 Qed.
@@ -293,7 +293,7 @@ generalize i;clear i;induction j;destruct T;simpl in H|-*;
 destruct i;simpl;try rewrite (IHj _ H);try (destruct i;simpl;congruence);reflexivity|| congruence.
 Qed.
 
-Record Store : Type :=  
+Record Store : Type :=
 mkStore  {index:positive;contents:Tree}.
 
 Definition empty := mkStore xH Tempty.
@@ -317,7 +317,7 @@ intros S W;induction W.
 unfold empty,index,get,contents;intros;apply Tget_Tempty.
 unfold index,get,push;simpl contents.
 intros i e;rewrite Tget_Tadd.
-rewrite (Gt_Psucc _ _ e). 
+rewrite (Gt_Psucc _ _ e).
 unfold get in IHW.
 apply IHW;apply Gt_Psucc;assumption.
 Qed.
@@ -336,8 +336,8 @@ apply get_Full_Gt; auto.
 apply Psucc_Gt.
 Qed.
 
-Theorem get_push_Full : 
-  forall i a S, Full S -> 
+Theorem get_push_Full :
+  forall i a S, Full S ->
   get i (push a S) =
   match (i ?= index S) Eq with
     Eq => PSome a
@@ -359,9 +359,9 @@ apply get_Full_Gt;auto.
 Qed.
 
 Lemma Full_push_compat : forall i a S, Full S ->
-forall x, get i S = PSome x -> 
+forall x, get i S = PSome x ->
  get i (push a S) = PSome x.
-intros i a S F x H. 
+intros i a S F x H.
 caseq ((i ?= index S) Eq);intro test.
 rewrite (Pcompare_Eq_eq _ _ test) in H.
 rewrite (get_Full_Eq _ F) in H;congruence.
@@ -372,7 +372,7 @@ assumption.
 rewrite (get_Full_Gt _ F) in H;congruence.
 Qed.
 
-Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty. 
+Lemma Full_index_one_empty : forall S, Full S -> index S = 1 -> S=empty.
 intros [ind cont] F one; inversion F.
 reflexivity.
 simpl index in one;assert (h:=Psucc_not_one (index S)).
@@ -382,7 +382,7 @@ Qed.
 Lemma push_not_empty: forall a S, (push a S) <> empty.
 intros a [ind cont];unfold push,empty.
 simpl;intro H;injection H; intros _ ; apply Psucc_not_one.
-Qed. 
+Qed.
 
 Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop :=
 match F with
@@ -390,7 +390,7 @@ F_empty => False
 | F_push a SS FF => x=a \/ In x SS FF
 end.
 
-Lemma get_In : forall (x:A) (S:Store) (F:Full S) i , 
+Lemma get_In : forall (x:A) (S:Store) (F:Full S) i ,
 get i S = PSome x -> In x S F.
 induction F.
 intro i;rewrite get_empty; congruence.
@@ -432,7 +432,7 @@ Implicit Arguments F_empty [A].
 Implicit Arguments F_push [A].
 Implicit Arguments In [A].
 
-Section Map. 
+Section Map.
 
 Variables A B:Set.
 
@@ -445,8 +445,8 @@ Tempty => Tempty
 | Branch1 a t1 t2 => Branch1 (f a) (Tmap t1) (Tmap t2)
 end.
 
-Lemma Tget_Tmap: forall T i, 
-Tget i (Tmap T)= match Tget i T with PNone => PNone 
+Lemma Tget_Tmap: forall T i,
+Tget i (Tmap T)= match Tget i T with PNone => PNone
 | PSome a => PSome (f a) end.
 induction T;intro i;case i;simpl;auto.
 Defined.
@@ -459,13 +459,13 @@ Defined.
 Definition map (S:Store A) : Store B :=
 mkStore (index S) (Tmap (contents S)).
 
-Lemma get_map: forall i S, 
-get i (map S)= match get i S with PNone => PNone 
+Lemma get_map: forall i S,
+get i (map S)= match get i S with PNone => PNone
 | PSome a => PSome (f a) end.
 destruct S;unfold get,map,contents,index;apply Tget_Tmap.
 Defined.
 
-Lemma map_push: forall a S, 
+Lemma map_push: forall a S,
 map (push a S) = push (f a) (map S).
 intros a S.
 case S.
@@ -474,7 +474,7 @@ intros;rewrite Tmap_Tadd;reflexivity.
 Defined.
 
 Theorem Full_map : forall S, Full S -> Full (map S).
-intros S F. 
+intros S F.
 induction F.
 exact F_empty.
 rewrite map_push;constructor 2;assumption.
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index 4b95097e2..0d1d09c73 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -23,7 +23,7 @@ Inductive form:Set:=
   Atom : positive -> form
 | Arrow : form -> form -> form
 | Bot
-| Conjunct : form -> form -> form 
+| Conjunct : form -> form -> form
 | Disjunct : form -> form -> form.
 
 Notation "[ n ]":=(Atom n).
@@ -39,7 +39,7 @@ match m with
   xI mm => match n with xI nn => pos_eq mm nn | _ => false end
 | xO mm => match n with xO nn => pos_eq mm nn | _ => false end
 | xH => match n with xH => true | _ => false end
-end. 
+end.
 
 Theorem pos_eq_refl : forall m n, pos_eq m n = true -> m = n.
 induction m;simpl;destruct n;congruence ||
@@ -49,32 +49,32 @@ Qed.
 Fixpoint form_eq (p q:form) {struct p} :bool :=
 match p with
   Atom m => match q with Atom n => pos_eq m n | _ => false end
-| Arrow p1 p2 => 
-match q with 
-  Arrow q1 q2 => form_eq p1 q1 && form_eq p2 q2 
+| Arrow p1 p2 =>
+match q with
+  Arrow q1 q2 => form_eq p1 q1 && form_eq p2 q2
 | _ => false end
 | Bot => match q with Bot => true | _ => false end
-| Conjunct p1 p2 => 
-match q with 
-  Conjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 
-| _ => false 
+| Conjunct p1 p2 =>
+match q with
+  Conjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2
+| _ => false
 end
-| Disjunct p1 p2 => 
-match q with 
-  Disjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2 
-| _ => false 
+| Disjunct p1 p2 =>
+match q with
+  Disjunct q1 q2 => form_eq p1 q1 && form_eq p2 q2
+| _ => false
 end
-end. 
+end.
 
 Theorem form_eq_refl: forall p q, form_eq p q = true -> p = q.
 induction p;destruct q;simpl;clean.
 intro h;generalize (pos_eq_refl _ _ h);congruence.
 caseq (form_eq p1 q1);clean.
-intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
 caseq (form_eq p1 q1);clean.
-intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
 caseq (form_eq p1 q1);clean.
-intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence. 
+intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
 Qed.
 
 Implicit Arguments form_eq_refl [p q].
@@ -102,16 +102,16 @@ end.
 
 Require Export BinPos.
 
-Ltac wipe := intros;simpl;constructor.  
+Ltac wipe := intros;simpl;constructor.
 
-Lemma compose0 : 
+Lemma compose0 :
 forall hyps F (A:Prop),
- A -> 
+ A ->
  (interp_ctx hyps F A).
 induction F;intros A H;simpl;auto.
 Qed.
 
-Lemma compose1 : 
+Lemma compose1 :
 forall hyps F (A B:Prop),
  (A -> B) ->
  (interp_ctx hyps F A) ->
@@ -120,9 +120,9 @@ induction F;intros A B H;simpl;auto.
 apply IHF;auto.
 Qed.
 
-Theorem compose2 : 
+Theorem compose2 :
 forall hyps F (A B C:Prop),
- (A -> B -> C) -> 
+ (A -> B -> C) ->
  (interp_ctx hyps F A) ->
  (interp_ctx hyps F B) ->
  (interp_ctx hyps F C).
@@ -130,10 +130,10 @@ induction F;intros A B C H;simpl;auto.
 apply IHF;auto.
 Qed.
 
-Theorem compose3 : 
+Theorem compose3 :
 forall hyps F (A B C D:Prop),
- (A -> B -> C -> D) -> 
- (interp_ctx hyps F A) -> 
+ (A -> B -> C -> D) ->
+ (interp_ctx hyps F A) ->
  (interp_ctx hyps F B) ->
  (interp_ctx hyps F C) ->
  (interp_ctx hyps F D).
@@ -148,7 +148,7 @@ induction F;simpl;intros;auto.
 apply compose1 with ([[a]]-> G);auto.
 Qed.
 
-Theorem project_In : forall hyps F g, 
+Theorem project_In : forall hyps F g,
 In g hyps F ->
 interp_ctx hyps F [[g]].
 induction F;simpl.
@@ -158,7 +158,7 @@ subst;apply compose0;simpl;trivial.
 apply compose1 with [[g]];auto.
 Qed.
 
-Theorem project : forall hyps F p g, 
+Theorem project : forall hyps F p g,
 get  p hyps = PSome g->
 interp_ctx hyps F [[g]].
 intros hyps F p g e; apply project_In.
@@ -186,23 +186,23 @@ Notation "hyps \ A" := (push A hyps) (at level 72,left associativity).
 
 Fixpoint check_proof (hyps:ctx) (gl:form) (P:proof) {struct P}: bool :=
  match P with
-   Ax i => 
+   Ax i =>
      match get i hyps with
          PSome F => form_eq F gl
  | _ => false
-    end 
+    end
 | I_Arrow p =>
    match gl with
       A  =>> B  => check_proof (hyps \ A) B p
-   | _ => false        
-    end 
+   | _ => false
+    end
 | E_Arrow i j p =>
    match get i hyps,get j hyps with
        PSome A,PSome (B =>>C) =>
          form_eq A B && check_proof (hyps \ C) (gl) p
     | _,_ => false
     end
-| D_Arrow i p1 p2 => 
+| D_Arrow i p1 p2 =>
    match get i hyps with
       PSome  ((A =>>B)=>>C) =>
      (check_proof ( hyps \ B =>> C \ A) B p1) && (check_proof (hyps \ C) gl p2)
@@ -219,12 +219,12 @@ Fixpoint check_proof (hyps:ctx) (gl:form) (P:proof) {struct P}: bool :=
       check_proof hyps A p1 && check_proof hyps B p2
       | _ => false
       end
-| E_And i p => 
+| E_And i p =>
    match get i hyps with
       PSome  (A //\\ B) => check_proof (hyps \ A \ B) gl p
     | _=> false
    end
-| D_And i p => 
+| D_And i p =>
    match get i hyps with
       PSome  (A //\\ B =>> C) => check_proof (hyps \ A=>>B=>>C) gl p
     | _=> false
@@ -245,7 +245,7 @@ Fixpoint check_proof (hyps:ctx) (gl:form) (P:proof) {struct P}: bool :=
   check_proof (hyps \ A) gl p1 && check_proof (hyps \ B) gl p2
   | _=> false
   end
-| D_Or i p => 
+| D_Or i p =>
    match get i hyps with
       PSome  (A \\// B =>> C) =>
       (check_proof (hyps \ A=>>C \ B=>>C) gl p)
@@ -253,10 +253,10 @@ Fixpoint check_proof (hyps:ctx) (gl:form) (P:proof) {struct P}: bool :=
    end
 | Cut A p1 p2 =>
   check_proof hyps A p1 && check_proof (hyps \ A) gl p2
-end. 
+end.
 
-Theorem interp_proof: 
-forall p hyps F gl, 
+Theorem interp_proof:
+forall p hyps F gl,
 check_proof hyps gl p = true -> interp_ctx hyps F [[gl]].
 
 induction p;intros hyps F gl.
@@ -281,7 +281,7 @@ intros f ef;caseq (get p0 hyps);clean.
 intros f0 ef0;destruct f0;clean.
 caseq (form_eq f f0_1);clean.
 simpl;intros e check_p1.
-generalize  (project  F ef) (project  F ef0) 
+generalize  (project  F ef) (project  F ef0)
 (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1);
 clear check_p1 IHp p p0 p1 ef ef0.
 simpl.
@@ -297,7 +297,7 @@ destruct f1;clean.
 caseq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean.
 intros check_p1 check_p2.
 generalize (project F ef)
-(IHp1 (hyps \ f1_2 =>> f2 \ f1_1)   
+(IHp1 (hyps \ f1_2 =>> f2 \ f1_1)
 (F_push f1_1 (hyps \ f1_2 =>> f2)
  (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1)
 (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2).
@@ -331,7 +331,7 @@ simpl;caseq (get p hyps);clean.
 intros f ef;destruct f;clean.
 destruct f1;clean.
 intro H;generalize  (project F ef)
-(IHp (hyps \ f1_1 =>> f1_2 =>> f2)  
+(IHp (hyps \ f1_1 =>> f1_2 =>> f2)
 (F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl.
 apply compose2;auto.
 
@@ -364,7 +364,7 @@ intros f ef;destruct f;clean.
 destruct f1;clean.
 intro check_p0;generalize (project F ef)
 (IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2)
-(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) 
+(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2)
  (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl.
 apply compose2;auto.
 
@@ -372,7 +372,7 @@ apply compose2;auto.
 Focus 1.
 simpl;caseq (check_proof hyps f p1);clean.
 intros check_p1 check_p2;
-generalize (IHp1 hyps F f check_p1) 
+generalize (IHp1 hyps F f check_p1)
 (IHp2 (hyps\f) (F_push f hyps F) gl check_p2);
 simpl; apply compose2;auto.
 Qed.
@@ -392,8 +392,8 @@ Parameters A B C D:Prop.
 Theorem toto:A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
 exact (Reflect (empty \ A \ B \ C)
 ([1] //\\ ([2] \\// [3]) =>> [1] //\\ [2] \\// [1] //\\ [3])
-(I_Arrow (E_And 1 (E_Or 3 
-  (I_Or_l (I_And (Ax 2) (Ax 4))) 
+(I_Arrow (E_And 1 (E_Or 3
+  (I_Or_l (I_And (Ax 2) (Ax 4)))
   (I_Or_r (I_And (Ax 2) (Ax 4))))))).
 Qed.
 Print toto.
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 1fee72a60..562e2e3bd 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -9,7 +9,7 @@
 (* $Id$ *)
 
 open Term
-open Util  
+open Util
 open Goptions
 
 type s_info=
@@ -54,12 +54,12 @@ let opt_pruning=
    optread=(fun () -> !pruning);
    optwrite=(fun b -> pruning:=b)}
 
-let _ = declare_bool_option opt_pruning 
+let _ = declare_bool_option opt_pruning
 
 type form=
     Atom of int
   | Arrow of form * form
-  | Bot 
+  | Bot
   | Conjunct of form * form
   | Disjunct of form * form
 
@@ -67,14 +67,14 @@ type tag=int
 
 let decomp_form=function
     Atom i -> Some (i,[])
-  | Arrow (f1,f2) -> Some (-1,[f1;f2]) 
+  | Arrow (f1,f2) -> Some (-1,[f1;f2])
   | Bot -> Some (-2,[])
   | Conjunct (f1,f2) -> Some (-3,[f1;f2])
   | Disjunct (f1,f2) -> Some (-4,[f1;f2])
 
 module Fmap=Map.Make(struct type t=form let compare=compare end)
 
-type sequent = 
+type sequent =
     {rev_hyps: form Intmap.t;
      norev_hyps: form Intmap.t;
      size:int;
@@ -103,14 +103,14 @@ type proof =
   | E_Or of int*proof*proof
   | D_Or of int*proof
   | Pop of int*proof
-      
+
 type rule =
     SAx of int
-  | SI_Arrow 
+  | SI_Arrow
   | SE_Arrow of int*int
   | SD_Arrow of int
   | SE_False of int
-  | SI_And 
+  | SI_And
   | SE_And of int
   | SD_And of int
   | SI_Or_l
@@ -132,9 +132,9 @@ let add_step s sub =
     | SI_Or_r,[p] -> I_Or_r p
     | SE_Or i,[p1;p2] -> E_Or(i,p1,p2)
     | SD_Or i,[p] -> D_Or(i,p)
-    | _,_ -> anomaly "add_step: wrong arity" 
-    
-type 'a with_deps = 
+    | _,_ -> anomaly "add_step: wrong arity"
+
+type 'a with_deps =
     {dep_it:'a;
      dep_goal:bool;
      dep_hyps:Intset.t}
@@ -148,7 +148,7 @@ type slice=
      changes_goal:bool;
      creates_hyps:Intset.t}
 
-type state = 
+type state =
     Complete of proof
   | Incomplete of sequent * slice list
 
@@ -164,15 +164,15 @@ let pop n prf =
     {prf with dep_it = nprf}
 
 let rec fill stack proof =
-  match stack with 
+  match stack with
       [] -> Complete proof.dep_it
     | slice::super ->
-	if 
+	if
 	  !pruning &&
 	  slice.proofs_done=[] &&
 	  not (slice.changes_goal && proof.dep_goal) &&
-	  not (Intset.exists 
-		 (fun i -> Intset.mem i proof.dep_hyps) 
+	  not (Intset.exists
+		 (fun i -> Intset.mem i proof.dep_hyps)
 		 slice.creates_hyps)
 	then
 	  begin
@@ -181,23 +181,23 @@ let rec fill stack proof =
 	    List.length slice.proofs_todo;
 	    let created_here=Intset.cardinal slice.creates_hyps in
 	      s_info.pruned_hyps<-s_info.pruned_hyps+
-	      List.fold_left 
-		(fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps) 
+	      List.fold_left
+		(fun sum dseq -> sum + Intset.cardinal dseq.dep_hyps)
 		created_here slice.proofs_todo;
 	    fill super (pop (Intset.cardinal slice.creates_hyps) proof)
 	  end
 	else
 	  let dep_hyps=
-	    Intset.union slice.needs_hyps 
+	    Intset.union slice.needs_hyps
 	      (Intset.diff proof.dep_hyps slice.creates_hyps) in
 	  let dep_goal=
-	    slice.needs_goal || 
+	    slice.needs_goal ||
 	    ((not slice.changes_goal) && proof.dep_goal) in
 	  let proofs_done=
 	    proof.dep_it::slice.proofs_done in
 	    match slice.proofs_todo with
 		[] ->
-		  fill super {dep_it = 
+		  fill super {dep_it =
 				add_step slice.step (List.rev proofs_done);
 			      dep_goal = dep_goal;
 			      dep_hyps = dep_hyps}
@@ -214,8 +214,8 @@ let rec fill stack proof =
 
 let append stack (step,subgoals) =
   s_info.created_steps<-s_info.created_steps+1;
-  match subgoals with 
-      [] -> 
+  match subgoals with
+      [] ->
 	s_info.branch_successes<-s_info.branch_successes+1;
 	fill stack {dep_it=add_step step.dep_it [];
 		    dep_goal=step.dep_goal;
@@ -239,10 +239,10 @@ let embed seq=
    dep_hyps=Intset.empty}
 
 let change_goal seq gl=
-    {seq with 
+    {seq with
        dep_it={seq.dep_it with gl=gl};
        dep_goal=true}
-	
+
 let add_hyp seqwd f=
   s_info.created_hyps<-s_info.created_hyps+1;
   let seq=seqwd.dep_it in
@@ -256,71 +256,71 @@ let add_hyp seqwd f=
     with Not_found -> seq.cnx,seq.right in
   let nseq=
     match f with
-	Bot -> 
-	  {seq with 
+	Bot ->
+	  {seq with
 	     left=left;
 	     right=right;
 	     size=num;
 	     abs=Some num;
 	     cnx=cnx}
       | Atom _ ->
-	  {seq with 
+	  {seq with
 	     size=num;
 	     left=left;
 	     right=right;
 	     cnx=cnx}
       | Conjunct (_,_) | Disjunct (_,_) ->
 	  {seq with
-	     rev_hyps=Intmap.add num f seq.rev_hyps; 
+	     rev_hyps=Intmap.add num f seq.rev_hyps;
 	     size=num;
 	     left=left;
 	     right=right;
 	     cnx=cnx}
       | Arrow (f1,f2) ->
 	  let ncnx,nright=
-	    try 
-	      let i = Fmap.find f1 seq.left in	  
+	    try
+	      let i = Fmap.find f1 seq.left in
 		(i,num,f1,f2)::cnx,right
 	    with Not_found ->
 	      cnx,(add_one_arrow num f1 f2 right) in
 	    match f1 with
 		Conjunct (_,_) | Disjunct (_,_) ->
 		  {seq with
-		     rev_hyps=Intmap.add num f seq.rev_hyps; 
+		     rev_hyps=Intmap.add num f seq.rev_hyps;
 		     size=num;
 		     left=left;
 		     right=nright;
 		     cnx=ncnx}
 	      | Arrow(_,_) ->
 		  {seq with
-		     norev_hyps=Intmap.add num f seq.norev_hyps; 
+		     norev_hyps=Intmap.add num f seq.norev_hyps;
 		     size=num;
 		     left=left;
 		     right=nright;
 		     cnx=ncnx}
-	      | _ -> 
+	      | _ ->
 		  {seq with
 		     size=num;
 		     left=left;
 		     right=nright;
 		     cnx=ncnx} in
-    {seqwd with 
+    {seqwd with
        dep_it=nseq;
        dep_hyps=Intset.add num seqwd.dep_hyps}
 
 exception Here_is of (int*form)
 
-let choose m= 
-  try 
+let choose m=
+  try
     Intmap.iter (fun i f -> raise (Here_is (i,f))) m;
     raise Not_found
-  with 
+  with
       Here_is (i,f) -> (i,f)
 
 
 let search_or seq=
   match seq.gl with
-      Disjunct (f1,f2) -> 
+      Disjunct (f1,f2) ->
 	[{dep_it = SI_Or_l;
 	  dep_goal = true;
 	  dep_hyps = Intset.empty},
@@ -333,19 +333,19 @@ let search_or seq=
 
 let search_norev seq=
   let goals=ref (search_or seq) in
-  let add_one i f= 
+  let add_one i f=
     match f with
 	Arrow (Arrow (f1,f2),f3) ->
-	  let nseq = 
+	  let nseq =
 	    {seq with norev_hyps=Intmap.remove i seq.norev_hyps} in
 	    goals:=
 	      ({dep_it=SD_Arrow(i);
 		dep_goal=false;
 		dep_hyps=Intset.singleton i},
-	       [add_hyp 
-		  (add_hyp 
-		     (change_goal (embed nseq) f2) 
-		     (Arrow(f2,f3))) 
+	       [add_hyp
+		  (add_hyp
+		     (change_goal (embed nseq) f2)
+		     (Arrow(f2,f3)))
 		  f1;
 		add_hyp (embed nseq) f3]):: !goals
       | _ -> anomaly "search_no_rev: can't happen" in
@@ -353,7 +353,7 @@ let search_norev seq=
     List.rev !goals
 
 let search_in_rev_hyps seq=
-  try 
+  try
     let i,f=choose seq.rev_hyps in
     let make_step step=
       {dep_it=step;
@@ -361,25 +361,25 @@ let search_in_rev_hyps seq=
        dep_hyps=Intset.singleton i} in
     let nseq={seq with rev_hyps=Intmap.remove i seq.rev_hyps} in
       match f with
-	  Conjunct (f1,f2) -> 
+	  Conjunct (f1,f2) ->
 	    [make_step (SE_And(i)),
 	     [add_hyp (add_hyp (embed nseq) f1) f2]]
 	| Disjunct (f1,f2) ->
 	    [make_step (SE_Or(i)),
 	     [add_hyp (embed nseq) f1;add_hyp (embed nseq) f2]]
-	| Arrow (Conjunct (f1,f2),f0) -> 
+	| Arrow (Conjunct (f1,f2),f0) ->
 	    [make_step (SD_And(i)),
 	     [add_hyp (embed nseq) (Arrow (f1,Arrow (f2,f0)))]]
 	| Arrow (Disjunct (f1,f2),f0) ->
 	    [make_step (SD_Or(i)),
 	     [add_hyp (add_hyp (embed nseq) (Arrow(f1,f0))) (Arrow (f2,f0))]]
-	| _ -> anomaly "search_in_rev_hyps: can't happen"	      
+	| _ -> anomaly "search_in_rev_hyps: can't happen"
   with
       Not_found -> search_norev seq
- 
+
 let search_rev seq=
   match seq.cnx with
-      (i,j,f1,f2)::next -> 
+      (i,j,f1,f2)::next ->
 	let nseq=
 	  match f1 with
 	      Conjunct (_,_) | Disjunct (_,_) ->
@@ -394,7 +394,7 @@ let search_rev seq=
 	    dep_goal=false;
 	    dep_hyps=Intset.add i (Intset.singleton j)},
 	   [add_hyp (embed nseq) f2]]
-    | [] -> 
+    | [] ->
 	match seq.gl with
 	    Arrow (f1,f2) ->
 	      [{dep_it=SI_Arrow;
@@ -410,19 +410,19 @@ let search_rev seq=
 
 let search_all seq=
   match seq.abs with
-      Some i -> 
+      Some i ->
 	[{dep_it=SE_False (i);
 	  dep_goal=false;
 	  dep_hyps=Intset.singleton i},[]]
     | None ->
-	try 
+	try
 	  let ax = Fmap.find seq.gl seq.left in
 	    [{dep_it=SAx (ax);
 	      dep_goal=true;
 	      dep_hyps=Intset.singleton ax},[]]
 	with Not_found -> search_rev seq
 
-let bare_sequent = embed 
+let bare_sequent = embed
 		     {rev_hyps=Intmap.empty;
 		      norev_hyps=Intmap.empty;
 		      size=0;
@@ -431,7 +431,7 @@ let bare_sequent = embed
 		      cnx=[];
 		      abs=None;
 		      gl=Bot}
-		     
+
 let init_state hyps gl=
   let init = change_goal bare_sequent gl in
   let goal=List.fold_right (fun (_,f,_) seq ->add_hyp seq f) hyps init in
@@ -448,12 +448,12 @@ let branching = function
       let _ =
 	match successors with
 	    [] -> s_info.branch_failures<-s_info.branch_failures+1
-	  | _::next ->  
+	  | _::next ->
 	      s_info.nd_branching<-s_info.nd_branching+List.length next in
 	List.map (append stack) successors
   | Complete prf -> anomaly "already succeeded"
 
-open Pp 
+open Pp
 
 let rec pp_form =
   function
@@ -470,13 +470,13 @@ and pp_and = function
 and pp_atom= function
     Bot -> str "#"
   | Atom n -> int n
-  | f -> str "(" ++ hv 2 (pp_form f) ++ str ")" 
+  | f -> str "(" ++ hv 2 (pp_form f) ++ str ")"
 
 let pr_form f = msg (pp_form f)
 
-let pp_intmap map = 
-  let pp=ref (str "") in  
-   Intmap.iter (fun i obj -> pp:= (!pp ++ 
+let pp_intmap map =
+  let pp=ref (str "") in
+   Intmap.iter (fun i obj -> pp:= (!pp ++
 		pp_form obj ++ cut ())) map;
     str "{ " ++ v 0 (!pp) ++ str " }"
 
@@ -486,17 +486,17 @@ let pp=ref (str "") in
   str "[ " ++ !pp ++ str "]"
 
 let pp_mapint map =
-  let pp=ref (str "") in  
-   Fmap.iter (fun obj l -> pp:= (!pp ++ 
-		pp_form obj ++ str " => " ++ 
-				 pp_list (fun (i,f) -> pp_form f) l ++ 
+  let pp=ref (str "") in
+   Fmap.iter (fun obj l -> pp:= (!pp ++
+		pp_form obj ++ str " => " ++
+				 pp_list (fun (i,f) -> pp_form f) l ++
 				 cut ()) ) map;
     str "{ " ++ vb 0 ++  (!pp) ++ str " }" ++ close ()
 
 let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2
 
 let pp_gl gl= cut () ++
-  str "{ " ++ vb 0 ++ 
+  str "{ " ++ vb 0 ++
 	      begin
 		match gl.abs with
 		    None -> str ""
@@ -504,38 +504,38 @@ let pp_gl gl= cut () ++
 	      end ++
   str "rev   =" ++ pp_intmap gl.rev_hyps ++ cut () ++
   str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++
-  str "arrows=" ++ pp_mapint gl.right ++ cut () ++ 
-  str "cnx   =" ++ pp_list pp_connect gl.cnx ++ cut () ++ 
+  str "arrows=" ++ pp_mapint gl.right ++ cut () ++
+  str "cnx   =" ++ pp_list pp_connect gl.cnx ++ cut () ++
   str "goal  =" ++ pp_form gl.gl ++ str " }" ++ close ()
 
-let pp = 
+let pp =
   function
       Incomplete(gl,ctx) -> msgnl (pp_gl gl)
     | _ -> msg (str "<complete>")
 
-let pp_info () = 
-  let count_info = 
+let pp_info () =
+  let count_info =
     if !pruning then
-	str "Proof steps : " ++ 
-	int s_info.created_steps ++ str " created / " ++ 
+	str "Proof steps : " ++
+	int s_info.created_steps ++ str " created / " ++
 	int s_info.pruned_steps ++ str " pruned" ++ fnl () ++
-	str "Proof branches : " ++ 
-	int s_info.created_branches ++ str " created / " ++ 
+	str "Proof branches : " ++
+	int s_info.created_branches ++ str " created / " ++
 	int s_info.pruned_branches ++ str " pruned" ++ fnl () ++
-	str "Hypotheses : " ++ 
-	int s_info.created_hyps ++ str " created / " ++ 
+	str "Hypotheses : " ++
+	int s_info.created_hyps ++ str " created / " ++
 	int s_info.pruned_hyps ++ str " pruned" ++ fnl ()
     else
 	str "Pruning is off" ++ fnl () ++
-	str "Proof steps : " ++ 
+	str "Proof steps : " ++
 	int s_info.created_steps ++ str " created" ++ fnl () ++
-	str "Proof branches : " ++ 
+	str "Proof branches : " ++
 	int s_info.created_branches ++ str " created" ++ fnl () ++
-	str "Hypotheses : " ++ 
+	str "Hypotheses : " ++
 	int s_info.created_hyps ++ str " created" ++ fnl () in
     msgnl
       ( str "Proof-search statistics :" ++ fnl () ++
-	count_info ++ 
+	count_info ++
 	str "Branch ends: " ++
 	int s_info.branch_successes ++ str " successes / " ++
 	int s_info.branch_failures ++ str " failures" ++ fnl () ++
@@ -543,4 +543,4 @@ let pp_info () =
 	int s_info.nd_branching ++ str " branches")
 
 
- 
+
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index a0e86b8d6..e52f6bbdc 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -11,10 +11,10 @@
 type form=
     Atom of int
   | Arrow of form * form
-  | Bot 
+  | Bot
   | Conjunct of form * form
   | Disjunct of form * form
-  
+
 type proof =
     Ax of int
   | I_Arrow of proof
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index b47bbaa93..23cb07050 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -18,24 +18,24 @@ open Evd
 open Tacmach
 open Proof_search
 
-let force count lazc = incr count;Lazy.force lazc 
+let force count lazc = incr count;Lazy.force lazc
 
 let step_count = ref 0
 
-let node_count = ref 0  
+let node_count = ref 0
 
-let logic_constant = 
-  Coqlib.gen_constant "refl_tauto" ["Init";"Logic"] 
+let logic_constant =
+  Coqlib.gen_constant "refl_tauto" ["Init";"Logic"]
 
 let li_False = lazy (destInd (logic_constant "False"))
 let li_and = lazy (destInd (logic_constant "and"))
 let li_or =  lazy (destInd (logic_constant "or"))
 
 let data_constant =
-  Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"] 
+  Coqlib.gen_constant "refl_tauto" ["Init";"Datatypes"]
 
-let l_true_equals_true = 
-  lazy (mkApp(logic_constant "refl_equal", 
+let l_true_equals_true =
+  lazy (mkApp(logic_constant "refl_equal",
         [|data_constant "bool";data_constant "true"|]))
 
 let pos_constant =
@@ -45,7 +45,7 @@ let l_xI = lazy (pos_constant "xI")
 let l_xO = lazy (pos_constant "xO")
 let l_xH = lazy (pos_constant "xH")
 
-let store_constant = 
+let store_constant =
   Coqlib.gen_constant "refl_tauto" ["rtauto";"Bintree"]
 
 let l_empty = lazy (store_constant "empty")
@@ -103,17 +103,17 @@ let rec make_form atom_env gls term =
   let normalize=special_nf gls in
   let cciterm=special_whd gls term  in
     match kind_of_term cciterm with
-	Prod(_,a,b) -> 
-	  if not (dependent (mkRel 1) b) && 
-	    Retyping.get_sort_family_of 
+	Prod(_,a,b) ->
+	  if not (dependent (mkRel 1) b) &&
+	    Retyping.get_sort_family_of
 	    (pf_env gls) (Tacmach.project gls) a = InProp
-	  then 
+	  then
 	    let fa=make_form atom_env gls a in
 	    let fb=make_form atom_env gls b in
 	      Arrow (fa,fb)
 	  else
 	    make_atom atom_env (normalize term)
-      | Cast(a,_,_) -> 
+      | Cast(a,_,_) ->
 	  make_form atom_env gls a
       | Ind ind ->
 	  if ind = Lazy.force li_False then
@@ -122,7 +122,7 @@ let rec make_form atom_env gls term =
 	    make_atom atom_env (normalize term)
       | App(hd,argv) when Array.length argv = 2 ->
 	  begin
-	    try 
+	    try
 	      let ind = destInd hd in
 		if ind = Lazy.force li_and then
 		  let fa=make_form atom_env gls argv.(0) in
@@ -139,103 +139,103 @@ let rec make_form atom_env gls term =
 
 let rec make_hyps atom_env gls lenv = function
     [] -> []
-  | (_,Some body,typ)::rest -> 
-      make_hyps atom_env gls (typ::body::lenv) rest  
+  | (_,Some body,typ)::rest ->
+      make_hyps atom_env gls (typ::body::lenv) rest
   | (id,None,typ)::rest ->
       let hrec=
 	make_hyps atom_env gls (typ::lenv) rest in
-	if List.exists (dependent (mkVar id)) lenv || 
-	  (Retyping.get_sort_family_of 
-	     (pf_env gls) (Tacmach.project gls) typ <> InProp) 
+	if List.exists (dependent (mkVar id)) lenv ||
+	  (Retyping.get_sort_family_of
+	     (pf_env gls) (Tacmach.project gls) typ <> InProp)
 	then
-	  hrec 
+	  hrec
 	else
 	  (id,make_form atom_env gls typ)::hrec
 
 let rec build_pos n =
-  if n<=1 then force node_count l_xH 
-  else if n land 1 = 0 then 
+  if n<=1 then force node_count l_xH
+  else if n land 1 = 0 then
     mkApp (force node_count l_xO,[|build_pos (n asr 1)|])
-  else 
+  else
     mkApp (force node_count l_xI,[|build_pos (n asr 1)|])
 
 let rec build_form = function
     Atom n -> mkApp (force node_count l_Atom,[|build_pos n|])
-  | Arrow (f1,f2) -> 
+  | Arrow (f1,f2) ->
       mkApp (force node_count l_Arrow,[|build_form f1;build_form f2|])
   | Bot -> force node_count l_Bot
-  | Conjunct (f1,f2) -> 
+  | Conjunct (f1,f2) ->
       mkApp (force node_count l_Conjunct,[|build_form f1;build_form f2|])
-  | Disjunct (f1,f2) -> 
+  | Disjunct (f1,f2) ->
       mkApp (force node_count l_Disjunct,[|build_form f1;build_form f2|])
 
-let rec decal k = function 
+let rec decal k = function
     [] -> k
-  | (start,delta)::rest -> 
+  | (start,delta)::rest ->
       if k>start then
 	k - delta
-      else 
+      else
 	decal k rest
 
 let add_pop size d pops=
   match pops with
       [] -> [size+d,d]
-    | (_,sum)::_ -> (size+sum,sum+d)::pops  
+    | (_,sum)::_ -> (size+sum,sum+d)::pops
 
-let rec build_proof pops size = 
+let rec build_proof pops size =
   function
       Ax i ->
 	mkApp (force step_count l_Ax,
 	       [|build_pos (decal i pops)|])
-      | I_Arrow p -> 
+      | I_Arrow p ->
 	  mkApp (force step_count l_I_Arrow,
 		 [|build_proof pops (size + 1) p|])
-      | E_Arrow(i,j,p) -> 
-	  mkApp (force step_count l_E_Arrow, 
+      | E_Arrow(i,j,p) ->
+	  mkApp (force step_count l_E_Arrow,
 		 [|build_pos (decal i pops);
 		   build_pos (decal j pops);
 		   build_proof pops (size + 1) p|])
-      | D_Arrow(i,p1,p2) -> 
-	  mkApp (force step_count l_D_Arrow, 
+      | D_Arrow(i,p1,p2) ->
+	  mkApp (force step_count l_D_Arrow,
 		 [|build_pos (decal i pops);
 		   build_proof pops (size + 2) p1;
 		   build_proof pops (size + 1) p2|])
-      | E_False i -> 
+      | E_False i ->
 	  mkApp (force step_count l_E_False,
 		 [|build_pos (decal i pops)|])
-      | I_And(p1,p2) -> 
-	  mkApp (force step_count l_I_And, 
+      | I_And(p1,p2) ->
+	  mkApp (force step_count l_I_And,
 		 [|build_proof pops size p1;
 		   build_proof pops size p2|])
-      | E_And(i,p) -> 
+      | E_And(i,p) ->
 	  mkApp (force step_count l_E_And,
 		 [|build_pos (decal i pops);
 		   build_proof pops (size + 2) p|])
-      | D_And(i,p) -> 
+      | D_And(i,p) ->
 	  mkApp (force step_count l_D_And,
 		 [|build_pos (decal i pops);
 		   build_proof pops (size + 1) p|])
-      | I_Or_l(p) -> 
+      | I_Or_l(p) ->
 	  mkApp (force step_count l_I_Or_l,
 		 [|build_proof pops size p|])
-      | I_Or_r(p) -> 
+      | I_Or_r(p) ->
 	  mkApp (force step_count l_I_Or_r,
 		 [|build_proof pops size p|])
       | E_Or(i,p1,p2) ->
-	  mkApp (force step_count l_E_Or, 
+	  mkApp (force step_count l_E_Or,
 		 [|build_pos (decal i pops);
 		   build_proof pops (size + 1) p1;
 		   build_proof pops (size + 1) p2|])
-      | D_Or(i,p) -> 
+      | D_Or(i,p) ->
 	  mkApp (force step_count l_D_Or,
 		 [|build_pos (decal i pops);
 		   build_proof pops (size + 2) p|])
       | Pop(d,p) ->
-	  build_proof (add_pop size d pops) size p 
-	    
+	  build_proof (add_pop size d pops) size p
+
 let build_env gamma=
-  List.fold_right (fun (p,_) e -> 
-		     mkApp(force node_count l_push,[|mkProp;p;e|])) 
+  List.fold_right (fun (p,_) e ->
+		     mkApp(force node_count l_push,[|mkProp;p;e|]))
     gamma.env (mkApp (force node_count l_empty,[|mkProp|]))
 
 open Goptions
@@ -249,7 +249,7 @@ let opt_verbose=
    optread=(fun () -> !verbose);
    optwrite=(fun b -> verbose:=b)}
 
-let _ = declare_bool_option opt_verbose 
+let _ = declare_bool_option opt_verbose
 
 let check = ref false
 
@@ -260,7 +260,7 @@ let opt_check=
    optread=(fun () -> !check);
    optwrite=(fun b -> check:=b)}
 
-let _ = declare_bool_option opt_check 
+let _ = declare_bool_option opt_check
 
 open Pp
 
@@ -269,34 +269,34 @@ let rtauto_tac gls=
   let gamma={next=1;env=[]} in
   let gl=gls.it.evar_concl in
   let _=
-    if Retyping.get_sort_family_of 
-      (pf_env gls) (Tacmach.project gls) gl <> InProp 
+    if Retyping.get_sort_family_of
+      (pf_env gls) (Tacmach.project gls) gl <> InProp
     then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
   let glf=make_form gamma gls gl in
-  let hyps=make_hyps gamma gls [gl] 
+  let hyps=make_hyps gamma gls [gl]
       (Environ.named_context_of_val gls.it.evar_hyps) in
   let formula=
-    List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in  
-  let search_fun = 
+    List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in
+  let search_fun =
     if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then
       Search.debug_depth_first
-    else 
+    else
       Search.depth_first in
-  let _ = 
+  let _ =
     begin
       reset_info ();
       if !verbose then
 	msgnl (str "Starting proof-search ...");
     end in
   let search_start_time = System.get_time () in
-  let prf = 
-    try project (search_fun (init_state [] formula)) 
+  let prf =
+    try project (search_fun (init_state [] formula))
     with Not_found ->
       errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in
   let search_end_time = System.get_time () in
   let _ = if !verbose then
     begin
-      msgnl (str "Proof tree found in " ++ 
+      msgnl (str "Proof tree found in " ++
 	     System.fmt_time_difference search_start_time search_end_time);
       pp_info ();
       msgnl (str "Building proof term ... ")
@@ -312,10 +312,10 @@ let rtauto_tac gls=
   let build_end_time=System.get_time () in
   let _ = if !verbose then
     begin
-      msgnl (str "Proof term built in " ++ 
+      msgnl (str "Proof term built in " ++
 	     System.fmt_time_difference build_start_time build_end_time ++
 	     fnl () ++
-	     str "Proof size : " ++ int !step_count ++ 
+	     str "Proof size : " ++ int !step_count ++
 	     str " steps" ++ fnl () ++
 	     str "Proof term size : " ++ int (!step_count+ !node_count) ++
 	     str " nodes (constants)" ++ fnl () ++
@@ -323,15 +323,15 @@ let rtauto_tac gls=
     end in
   let tac_start_time = System.get_time () in
   let result=
-    if !check then 
+    if !check then
       Tactics.exact_check term gls
     else
       Tactics.exact_no_check term gls in
   let tac_end_time = System.get_time () in
-  let _ = 
+  let _ =
     if !check then msgnl (str "Proof term type-checking is on");
     if !verbose then
-      msgnl (str "Internal tactic executed in " ++ 
+      msgnl (str "Internal tactic executed in " ++
 	     System.fmt_time_difference tac_start_time tac_end_time) in
     result