bug 17392: remove trailing whitespace in source files

15 files changed, 75 insertions, 75 deletions

diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 3b77f135..3d1dd754 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -11,13 +11,13 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* Util functions used for the expansion of built-ins and some 
+(* Util functions used for the expansion of built-ins and some
    pseudo-instructions *)
 
 open Asm
 open AST
 open Camlcoq
-       
+
 (* Buffering the expanded code *)
 
 let current_code = ref ([]: instruction list)
@@ -25,7 +25,7 @@ let current_code = ref ([]: instruction list)
 let emit i = current_code := i :: !current_code
 
 (* Generation of fresh labels *)
-							  
+
 let dummy_function = { fn_code = []; fn_sig = signature_main }
 let current_function = ref dummy_function
 let next_label = ref (None: label option)
@@ -46,7 +46,7 @@ let new_label () =
     next_label := Some (P.succ lbl);
     lbl
 
-		     
+
 let set_current_function f =
   current_function := f; next_label := None; current_code := []
 
@@ -64,7 +64,7 @@ let expand_scope id lbl oldscopes newscopes =
   List.iter (fun i -> Debug.open_scope id i lbl) opening;
   List.iter (fun i -> Debug.close_scope id i lbl) closing
 
-let translate_annot sp preg_to_dwarf annot = 
+let translate_annot sp preg_to_dwarf annot =
   let rec aux = function
     | BA x -> Some (sp,BA (preg_to_dwarf x))
     | BA_int _
@@ -75,7 +75,7 @@ let translate_annot sp preg_to_dwarf annot =
     | BA_addrglobal _
     | BA_loadstack _ -> None
     | BA_addrstack ofs -> Some (sp,BA_addrstack ofs)
-    | BA_splitlong (hi,lo) -> 
+    | BA_splitlong (hi,lo) ->
         begin
           match (aux hi,aux lo) with
           | Some (_,hi) ,Some (_,lo) -> Some (sp,BA_splitlong (hi,lo))
@@ -84,11 +84,11 @@ let translate_annot sp preg_to_dwarf annot =
   (match annot with
   | [] -> None
   | a::_ -> aux a)
-    
+
 
 let expand_debug id sp preg simple l =
   let get_lbl = function
-    | None -> 
+    | None ->
         let lbl = new_label () in
         emit (Plabel lbl);
         lbl
@@ -99,12 +99,12 @@ let expand_debug id sp preg simple l =
         let kind = (P.to_int kind) in
         begin
           match kind with
-          | 1-> 
+          | 1->
               emit i;aux lbl scopes rest
           | 2 ->
               aux  lbl scopes rest
           | 3 ->
-             begin 
+             begin
                match translate_annot sp preg args with
                | Some a ->
                    let lbl = get_lbl lbl in
@@ -132,7 +132,7 @@ let expand_debug id sp preg simple l =
           | _ ->
               aux None scopes rest
         end
-    | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest 
+    | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
   let rec move_debug acc bcc = function
diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index 7ed5b4ab..6695b6b7 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -21,8 +21,8 @@ exception Error of string
 }
 
 let blank = [' ' '\009' '\012' '\010' '\013']
-let floatlit = 
- ("-"? (['0'-'9'] ['0'-'9' '_']* 
+let floatlit =
+ ("-"? (['0'-'9'] ['0'-'9' '_']*
   ('.' ['0'-'9' '_']* )?
   (['e' 'E'] ['+' '-']? ['0'-'9'] ['0'-'9' '_']*)? )) | "inf" | "nan"
 let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '_' '$' '0'-'9']*
@@ -69,7 +69,7 @@ rule token = parse
   | "floatofintu"    { FLOATOFINTU }
   | "floatoflong"  { FLOATOFLONG }
   | "floatoflongu" { FLOATOFLONGU }
-  | "goto"  { GOTO } 
+  | "goto"  { GOTO }
   | ">"    { GREATER }
   | ">f"    { GREATERF }
   | ">l"    { GREATERL }
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index b48a486e..5b79cde8 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -13,7 +13,7 @@
 /*                                                                     */
 /* *********************************************************************/
 
-/* Note that this compiles a superset of the language defined by the AST, 
+/* Note that this compiles a superset of the language defined by the AST,
    including function calls in expressions, matches, while statements, etc. */
 
 %{
@@ -123,7 +123,7 @@ let mkeval e =
       let c1 = convert_rexpr e1 in
       let cl = convert_rexpr_list el in
       prepend_seq !convert_accu (Scall(None, sg, c1, cl))
-  | Rbuiltin(sg, pef, el) -> 
+  | Rbuiltin(sg, pef, el) ->
       let ef = mkef sg pef in
       let cl = convert_rexpr_list el in
       prepend_seq !convert_accu (Sbuiltin(None, ef, cl))
@@ -322,9 +322,9 @@ let mkmatch expr cases =
 %token LESSLESSL
 %token LONG
 %token <int64> LONGLIT
-%token LONGOFINT 
+%token LONGOFINT
 %token LONGOFINTU
-%token LONGOFFLOAT 
+%token LONGOFFLOAT
 %token LONGUOFFLOAT
 %token LOOP
 %token LPAREN
@@ -375,7 +375,7 @@ let mkmatch expr cases =
 %left CARET CARETL
 %left AMPERSAND AMPERSANDL
 %left EQUALEQUAL BANGEQUAL LESS LESSEQUAL GREATER GREATEREQUAL EQUALEQUALU BANGEQUALU LESSU LESSEQUALU GREATERU GREATEREQUALU EQUALEQUALF BANGEQUALF LESSF LESSEQUALF GREATERF GREATEREQUALF EQUALEQUALL BANGEQUALL LESSL LESSEQUALL GREATERL GREATEREQUALL EQUALEQUALLU BANGEQUALLU LESSLU LESSEQUALLU GREATERLU GREATEREQUALLU
-%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU 
+%left LESSLESS GREATERGREATER GREATERGREATERU LESSLESSL GREATERGREATERL GREATERGREATERLU
 %left PLUS PLUSF PLUSL MINUS MINUSF MINUSL
 %left STAR SLASH PERCENT STARF SLASHF SLASHU PERCENTU STARL SLASHL SLASHLU PERCENTL PERCENTLU
 %nonassoc BANG TILDE TILDEL p_uminus ABSF INTOFFLOAT INTUOFFLOAT FLOATOFINT FLOATOFINTU INT8S INT8U INT16S INT16U FLOAT32 INTOFLONG LONGOFINT LONGOFINTU LONGOFFLOAT LONGUOFFLOAT FLOATOFLONG FLOATOFLONGU
@@ -432,12 +432,12 @@ init_data_list:
     /* empty */                                 { [] }
    | init_data_list_1                           { $1 }
  ;
- 
+
 init_data_list_1:
      init_data                                   { [$1] }
    | init_data_list_1 COMMA init_data            { $3 :: $1 }
  ;
- 
+
 init_data:
      INT8 INTLIT                                 { Init_int8 (coqint_of_camlint $2) }
    | INT16 INTLIT                                { Init_int16 (coqint_of_camlint $2) }
@@ -453,7 +453,7 @@ init_data:
    | LBRACKET INTLIT RBRACKET                    { Init_space (Z.of_sint32 $2) }
    | INTLIT LPAREN STRINGLIT RPAREN              { Init_addrof (intern_string $3, coqint_of_camlint $1) }
  ;
- 
+
 /* Procedures */
 
 proc:
@@ -472,14 +472,14 @@ proc:
                         fn_vars = List.rev (tmp @ $9);
                         fn_stackspace = $8;
                         fn_body = $10 })) }
-  | EXTERN STRINGLIT COLON signature 
+  | EXTERN STRINGLIT COLON signature
       { (intern_string $2, Gfun(External(EF_external(intern_string $2,$4)))) }
   | EXTERN STRINGLIT EQUAL eftoks COLON signature
       { (intern_string $2, Gfun(External(mkef $6 $4))) }
 ;
 
 signature:
-    type_ 
+    type_
                { {sig_args = []; sig_res = Some $1; sig_cc = cc_default} }
   | VOID
                { {sig_args = []; sig_res = None; sig_cc = cc_default} }
diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index aacbf86f..72bf9cb4 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -323,7 +323,7 @@ let rec type_stmt env blk ret s =
   | Sreturn (Some e) ->
       begin match ret with
       | None -> raise (Error "return with argument")
-      | Some tret -> 
+      | Some tret ->
           begin try
             unify (type_expr env [] e) (ty_of_typ tret)
           with Error s ->
diff --git a/backend/IRC.ml b/backend/IRC.ml
index dcd8624a..eb677069 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -163,7 +163,7 @@ module DLinkMove = struct
   type t = move
   let make state =
     let rec empty =
-      { src = DLinkNode.dummy; dst = DLinkNode.dummy; 
+      { src = DLinkNode.dummy; dst = DLinkNode.dummy;
         mstate = state; mprev = empty; mnext = empty }
     in empty
   let dummy = make CoalescedMoves
@@ -301,7 +301,7 @@ let init costs =
     worklistMoves = DLinkMove.make WorklistMoves;
     activeMoves = DLinkMove.make ActiveMoves
   }
-  
+
 (* Create nodes corresponding to XTL variables *)
 
 let weightedSpillCost st =
@@ -312,7 +312,7 @@ let weightedSpillCost st =
 let newNodeOfReg g r ty =
   let st = g.stats_of_reg r in
   g.nextIdent <- g.nextIdent + 1;
-  { ident = g.nextIdent; typ = ty; 
+  { ident = g.nextIdent; typ = ty;
     var = V(r, ty);
     regclass = if st.cost >= 0 then class_of_type ty else no_spill_class;
     accesses = st.usedefs;
@@ -328,7 +328,7 @@ let newNodeOfReg g r ty =
 let newNodeOfLoc g l =
   let ty = Loc.coq_type l in
   g.nextIdent <- g.nextIdent + 1;
-  { ident = g.nextIdent; typ = ty; 
+  { ident = g.nextIdent; typ = ty;
     var = L l; regclass = class_of_type ty;
     accesses = 0; spillcost = 0.0;
     adjlist = []; degree = 0; movelist = []; extra_adj = []; extra_pref = [];
@@ -608,9 +608,9 @@ let canCoalesceGeorge g u v =
 -  If [u] is precolored, use George's criterion.
 -  If [u] is not precolored, use Briggs's criterion.
 
-   As noted by Hailperin, for non-precolored nodes, George's criterion 
+   As noted by Hailperin, for non-precolored nodes, George's criterion
    is incomparable with Briggs's: there are cases where G says yes
-   and B says no.  Typically, [u] is a long-lived variable with many 
+   and B says no.  Typically, [u] is a long-lived variable with many
    interferences, and [v] is a short-lived temporary copy of [u]
    that has no more interferences than [u].  Coalescing [u] and [v]
    is "weakly safe" in Hailperin's terminology: [u] is no harder to color,
@@ -690,7 +690,7 @@ let coalesce g =
     combine g u v;
     addWorkList g u
   end else begin
-    DLinkMove.insert m g.activeMoves    
+    DLinkMove.insert m g.activeMoves
   end
 
 (* Freeze moves associated with node [u] *)
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml
index ef268562..71ee2e56 100644
--- a/backend/Linearizeaux.ml
+++ b/backend/Linearizeaux.ml
@@ -26,7 +26,7 @@ let enumerate_aux f reach =
     (fun pc nodes ->
       if PMap.get pc reach
       then Coq_cons (pc, nodes)
-      else nodes) 
+      else nodes)
     f.fn_nextpc
 ***)
 
@@ -100,7 +100,7 @@ let basic_blocks f joins =
   (* end_block: record block that we just discovered *)
   and end_block blk minpc =
     blocks := (minpc, List.rev blk) :: !blocks
-  in 
+  in
     start_block f.fn_entrypoint; !blocks
 
 (* Flatten basic blocks in decreasing order of minpc *)
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 594b43b7..e7c945e3 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -38,7 +38,7 @@ module Printer(Target:TARGET) =
 
     let print_location oc loc =
       if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
-          
+
     let print_function oc name fn =
       Hashtbl.clear current_function_labels;
       Target.reset_constants ();
@@ -66,7 +66,7 @@ module Printer(Target:TARGET) =
       Target.print_jumptable oc jmptbl;
       if !Clflags.option_g then
         Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels
-    
+
     let print_init_data oc name id =
       if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
           && List.for_all (function Init_int8 _ -> true | _ -> false) id
@@ -74,7 +74,7 @@ module Printer(Target:TARGET) =
         fprintf oc "	.ascii	\"%s\"\n" (PrintCsyntax.string_of_init id)
       else
         List.iter (Target.print_init oc) id
- 
+
     let print_var oc name v =
       match v.gvar_init with
       | [] -> ()
@@ -101,7 +101,7 @@ module Printer(Target:TARGET) =
             let sz =
               match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
             Target.print_comm_symb oc sz name align
-                            
+
     let print_globdef oc (name,gdef) =
       match gdef with
       | Gfun (Internal code) -> print_function oc name code
@@ -116,7 +116,7 @@ module Printer(Target:TARGET) =
         let symbol = Target.symbol
       end
 
-    module DebugPrinter = DwarfPrinter (DwarfTarget)     
+    module DebugPrinter = DwarfPrinter (DwarfTarget)
   end
 
 let print_program oc p db =
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 78399c04..4a612c26 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -98,7 +98,7 @@ let elf_symbol_offset oc (symb, ofs) =
 let elf_print_fun_info oc name =
   fprintf oc "	.type	%a, @function\n" elf_symbol name;
   fprintf oc "	.size	%a, . - %a\n" elf_symbol name elf_symbol name
-   
+
 let elf_print_var_info oc name =
   fprintf oc "	.type	%a, @object\n" elf_symbol name;
   fprintf oc "	.size	%a, . - %a\n" elf_symbol name elf_symbol name
@@ -109,20 +109,20 @@ let cfi_startproc =
     (fun oc -> fprintf oc "	.cfi_startproc\n")
   else
     (fun _ -> ())
-      
+
 let cfi_endproc =
   if Configuration.asm_supports_cfi then
     (fun oc -> fprintf oc "	.cfi_endproc\n")
   else
     (fun _ -> ())
-      
-      
+
+
 let cfi_adjust =
   if Configuration.asm_supports_cfi then
        (fun oc delta -> fprintf oc "	.cfi_adjust_cfa_offset	%ld\n" delta)
   else
     (fun _ _ -> ())
-      
+
 let cfi_rel_offset =
   if Configuration.asm_supports_cfi then
     (fun oc reg ofs -> fprintf oc "	.cfi_rel_offset	%s, %ld\n" reg ofs)
@@ -211,7 +211,7 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args =
                  comment print_debug_args args;
   | _ ->
       ()
-					    
+
 (** Inline assembly *)
 
 let print_asm_argument print_preg oc modifier = function
@@ -256,7 +256,7 @@ let print_inline_asm print_preg oc txt sg args res =
 (** Print CompCert version and command-line as asm comment *)
 
 let print_version_and_options oc comment =
-  let version_string =  
+  let version_string =
     if Version.buildnr <> "" && Version.tag <> "" then
       sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
     else
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 19f4c839..9b6b1488 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -139,7 +139,7 @@ let rec expr p (prec, e) =
     if assoc = LtoR
     then (prec', prec' + 1)
     else (prec' + 1, prec') in
-  if prec' < prec 
+  if prec' < prec
   then fprintf p "@[<hov 2>("
   else fprintf p "@[<hov 2>";
   begin match e with
@@ -238,14 +238,14 @@ let rec print_stmt p s =
                 print_expr_list (true, el)
 	        print_sig (ef_sig ef)
   | Sbuiltin(Some id, ef, el) ->
-      fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]) : @[<hov 0>%a@];@]" 
+      fprintf p "@[<hv 2>%s =@ builtin %s@,(@[<hov 0>%a@]) : @[<hov 0>%a@];@]"
                 (ident_name id)
                 (name_of_external ef)
                 print_expr_list (true, el)
 	        print_sig (ef_sig ef)
   | Sseq(s1,s2) when just_skips s1 && just_skips s2 ->
       ()
-  | Sseq(s1, s2) when just_skips s1 -> 
+  | Sseq(s1, s2) when just_skips s1 ->
       print_stmt p s2
   | Sseq(s1, s2) when just_skips s2 ->
       print_stmt p s1
@@ -277,7 +277,7 @@ let rec print_stmt p s =
         (if long then "l" else "") print_expr e;
       List.iter
         (fun (n, x) ->
-           fprintf p "@ case %s%s: exit %d;" 
+           fprintf p "@ case %s%s: exit %d;"
                      (Z.to_string n)
                      (if long then "LL" else "")
                      (Nat.to_int x))
@@ -334,12 +334,12 @@ let print_init_data p = function
 let rec print_init_data_list p = function
   | [] -> ()
   | [item] -> print_init_data p item
-  | item::rest -> 
+  | item::rest ->
       (print_init_data p item;
        fprintf p ",";
        print_init_data_list p rest)
 
-let print_globvar p gv = 
+let print_globvar p gv =
   if (gv.gvar_readonly) then
     fprintf p "readonly ";
   if (gv.gvar_volatile) then
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 78ce1816..f2242c13 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -99,7 +99,7 @@ let print_function pp id f =
       (List.rev_map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
-  print_succ pp f.fn_entrypoint 
+  print_succ pp f.fn_entrypoint
     (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1);
   List.iter (print_instruction pp) instrs;
   fprintf pp "}\n\n"
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index bb67dc96..dd8434da 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -71,7 +71,7 @@ let liveset pp lv =
   fprintf pp "{";
   VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r)
                     | L l -> ())
-    lv;                  
+    lv;
   fprintf pp " }"
 
 let print_succ pp s dfl =
@@ -145,7 +145,7 @@ let print_function pp ?alloc ?live f =
       (List.map
         (fun (pc, i) -> (P.to_int pc, i))
         (PTree.elements f.fn_code)) in
-  print_succ pp f.fn_entrypoint 
+  print_succ pp f.fn_entrypoint
     (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1);
   List.iter (print_block pp) instrs;
   fprintf pp "}\n\n";
diff --git a/backend/RTLgenaux.ml b/backend/RTLgenaux.ml
index e3373bf9..045299d4 100644
--- a/backend/RTLgenaux.ml
+++ b/backend/RTLgenaux.ml
@@ -72,7 +72,7 @@ let size_eos = function
 let rec size_stmt = function
   | Sskip -> 0
   | Sassign(id, a) -> size_expr a
-  | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src 
+  | Sstore(chunk, addr, args, src) -> 1 + size_exprs args + size_expr src
   | Scall(optid, sg, eos, args) ->
       3 + size_eos eos + size_exprs args + length_exprs args
   | Stailcall(sg, eos, args) ->
@@ -91,6 +91,6 @@ let rec size_stmt = function
   | Slabel(lbl, s) -> size_stmt s
   | Sgoto lbl -> 1
 
-let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = 
+let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) =
   size_stmt ifso > size_stmt ifnot
 
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 76288fb5..a5fa8cd7 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -234,7 +234,7 @@ let block_of_RTL_instr funsig tyenv = function
       and res' = vmregs (loc_result sg) in
       xparmove (expand_regs tyenv args) args'
        (Xcall(sg, sum_left_map (vreg tyenv) ros, args', res') ::
-         xparmove res' (expand_regs tyenv [res]) 
+         xparmove res' (expand_regs tyenv [res])
            [Xbranch s])
   | RTL.Itailcall(sg, ros, args) ->
       let args' = vlocs (loc_arguments sg) in
@@ -273,7 +273,7 @@ let function_of_RTL_function f tyenv =
   let xc = PTree.map1 (block_of_RTL_instr f.RTL.fn_sig tyenv) f.RTL.fn_code in
   (* Add moves for function parameters *)
   let pc_entrypoint = next_pc f in
-  let b_entrypoint = 
+  let b_entrypoint =
      xparmove (vlocs (loc_parameters f.RTL.fn_sig))
               (expand_regs tyenv f.RTL.fn_params)
               [Xbranch f.RTL.fn_entrypoint] in
@@ -465,7 +465,7 @@ let spill_costs f =
           let c1 = st.cost + amount in
           let c2 = if c1 >= 0 then c1 else max_int (* overflow *) in
           st.cost <- c2
-        end;           
+        end;
         st.usedefs <- st.usedefs + uses in
 
   let charge_list amount uses vl =
@@ -624,7 +624,7 @@ let add_interfs_instr g instr live =
       add_interfs_destroyed g (VSet.remove res live) (destroyed_by_op op)
   | Xload(chunk, addr, args, dst) ->
       add_interfs_def g dst live;
-      add_interfs_destroyed g (VSet.remove dst live) 
+      add_interfs_destroyed g (VSet.remove dst live)
                               (destroyed_by_load chunk addr)
   | Xstore(chunk, addr, args, src) ->
       add_interfs_destroyed g live (destroyed_by_store chunk addr)
@@ -655,7 +655,7 @@ let add_interfs_instr g instr live =
             | Some mr ->
                 add_interfs_list_mreg g vargs mr;
                 add_interfs_list_mreg g vres mr)
-            clob          
+            clob
       | _ -> ()
       end
   | Xbranch s ->
@@ -776,7 +776,7 @@ let add v t eqs = (v, t, 0) :: eqs
 
 let kill x eqs =
   List.filter (fun (v, t, date) -> v <> x && t <> x) eqs
-  
+
 let reload_var tospill eqs v =
   if not (VSet.mem v tospill) then
     (v, [], eqs)
@@ -845,7 +845,7 @@ let rec trim count eqs =
   if count <= 0 then [] else
     match eqs with
     | [] -> []
-    | (v, t, date) :: eqs' -> 
+    | (v, t, date) :: eqs' ->
         if date <= !max_age
         then (v, t, date + 1) :: trim (count - 1) eqs'
         else []
@@ -882,7 +882,7 @@ let spill_instr tospill eqs instr =
           | true, false ->
               let tmp = new_temp (typeof res) in
               let (argl', c1, eqs1) = reload_vars tospill eqs argl in
-              (c1 @ [Xmove(arg1, tmp); Xop(op, tmp :: argl', tmp); Xspill(tmp, res)], 
+              (c1 @ [Xmove(arg1, tmp); Xop(op, tmp :: argl', tmp); Xspill(tmp, res)],
                add res tmp (kill res eqs1))
           | false, true ->
               let eqs1 = add arg1 res (kill res eqs) in
@@ -890,13 +890,13 @@ let spill_instr tospill eqs instr =
               (Xreload(arg1, res) :: c1 @ [Xop(op, res :: argl', res)],
                kill res eqs2)
           | true, true ->
-              let tmp = new_temp (typeof res) in              
+              let tmp = new_temp (typeof res) in
               let eqs1 = add arg1 tmp eqs in
               let (argl', c1, eqs2) = reload_vars tospill eqs1 argl in
               (Xreload(arg1, tmp) :: c1 @ [Xop(op, tmp :: argl', tmp); Xspill(tmp, res)],
                add res tmp (kill tmp (kill res eqs2)))
           end
-      end          
+      end
   | Xload(chunk, addr, args, dst) ->
       let (args', c1, eqs1) = reload_vars tospill eqs args in
       let (dst', c2, eqs2) = save_var tospill eqs1 dst in
@@ -1047,7 +1047,7 @@ let transl_instr alloc instr k =
           if rarg1 = rres then
             LTL.Lop(op, rargs, rres) :: k
           else
-            LTL.Lop(Omove, [rarg1], rres) :: 
+            LTL.Lop(Omove, [rarg1], rres) ::
             LTL.Lop(op, rres :: rargl, rres) :: k
       end
   | Xload(chunk, addr, args, dst) ->
@@ -1079,7 +1079,7 @@ let transl_function fn alloc =
   { LTL.fn_sig = fn.fn_sig;
     LTL.fn_stacksize = fn.fn_stacksize;
     LTL.fn_entrypoint = fn.fn_entrypoint;
-    LTL.fn_code = PTree.map1 (transl_block alloc) fn.fn_code 
+    LTL.fn_code = PTree.map1 (transl_block alloc) fn.fn_code
   }
 
 
@@ -1113,7 +1113,7 @@ and more_rounds f ts count =
       fprintf !pp "--- Remain to be spilled:\n";
       VSet.iter (fun v -> fprintf !pp "%a " PrintXTL.var v) ts';
       fprintf !pp "\n\n"
-    end;      
+    end;
     more_rounds f (VSet.union ts ts') (count + 1)
   end
 
@@ -1148,7 +1148,7 @@ let regalloc f =
       | Timeout ->
           Error(msg (coqstring_of_camlstring "Spilling fails to converge"))
       | Type_error_at pc ->
-          Error [MSG(coqstring_of_camlstring "Ill-typed XTL code at PC "); 
+          Error [MSG(coqstring_of_camlstring "Ill-typed XTL code at PC ");
                  POS pc]
       | Bad_LTL ->
           Error(msg (coqstring_of_camlstring "Bad LTL after spilling"))
diff --git a/backend/Splitting.ml b/backend/Splitting.ml
index 97b26a50..17b8098d 100644
--- a/backend/Splitting.ml
+++ b/backend/Splitting.ml
@@ -39,9 +39,9 @@ let rec repr lr =
   | Link lr' -> let lr'' = repr lr' in lr.kind <- Link lr''; lr''
   | _ -> lr
 
-let same_range lr1 lr2 = 
-  lr1 == lr2 || (* quick test for speed *) 
-  repr lr1 == repr lr2 (* the real test *) 
+let same_range lr1 lr2 =
+  lr1 == lr2 || (* quick test for speed *)
+  repr lr1 == repr lr2 (* the real test *)
 
 let unify lr1 lr2 =
   let lr1 = repr lr1 and lr2 = repr lr2 in
diff --git a/backend/XTL.ml b/backend/XTL.ml
index dde9bdb0..2ddbc50a 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -186,7 +186,7 @@ let type_block blk =
 let type_function f =
   PTree.fold
     (fun () pc blk ->
-       try 
+       try
          type_block blk
        with Type_error ->
          raise (Type_error_at pc))