diff --git a/sat/res.ml b/sat/res.ml
index 5712d6e9..5cd34a5f 100644
--- a/sat/res.ml
+++ b/sat/res.ml
@@ -8,255 +8,261 @@ module type S = Res_intf.S
 
 module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
 
-    (* Type definitions *)
-    type lemma = Proof.proof
-    type clause = St.clause
-    type atom = St.atom
-    type int_cl = clause * St.atom list
+  (* Type definitions *)
+  type lemma = Proof.proof
+  type clause = St.clause
+  type atom = St.atom
+  type int_cl = clause * St.atom list
 
-    type node =
-        | Assumption
-        | Lemma of lemma
-        | Resolution of atom * int_cl * int_cl
-        (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
+  type node =
+    | Assumption
+    | Lemma of lemma
+    | Resolution of atom * int_cl * int_cl
+    (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *)
 
-    exception Resolution_error of string
+  exception Resolution_error of string
 
-    (* Proof graph *)
-    let hash_cl cl =
-        Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl)
+  (* Proof graph *)
+  let hash_cl cl =
+    Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl)
 
-    let equal_cl cl_c cl_d =
-        try
-            List.for_all2 (==) cl_c cl_d
-        with Invalid_argument _ ->
-            false
+  let equal_cl cl_c cl_d =
+    try
+      List.for_all2 (==) cl_c cl_d
+    with Invalid_argument _ ->
+      false
 
-    module H = Hashtbl.Make(struct
-        type t = St.atom list
-        let hash = hash_cl
-        let equal = equal_cl
+  module H = Hashtbl.Make(struct
+      type t = St.atom list
+      let hash = hash_cl
+      let equal = equal_cl
     end)
-    let proof : node H.t = H.create 1007;;
+  let proof : node H.t = H.create 1007;;
 
-    (* Misc functions *)
-    let equal_atoms a b = St.(a.aid) = St.(b.aid)
-    let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
+  (* Misc functions *)
+  let equal_atoms a b = St.(a.aid) = St.(b.aid)
+  let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid)
 
-    (* Compute resolution of 2 clauses *)
-    let resolve l =
-        let rec aux resolved acc = function
-            | [] -> resolved, acc
-            | [a] -> resolved, a :: acc
-            | a :: b :: r ->
-                    if equal_atoms a b then
-                        aux resolved (a :: acc) r
-                    else if equal_atoms St.(a.neg) b then
-                        aux (St.(a.var.pa) :: resolved) acc r
-                    else
-                        aux resolved (a :: acc) (b :: r)
-        in
-        let resolved, new_clause = aux [] [] l in
-        resolved, List.rev new_clause
+  (* Printing functions *)
+  let print_atom fmt a =
+    Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1)
 
-    let to_list c =
-        let v = St.(c.atoms) in
-        let l = ref [] in
-        for i = 0 to Vec.size v - 1 do
-            l := (Vec.get v i) :: !l
-        done;
-        let l, res = resolve (List.sort_uniq compare_atoms !l) in
-        if l <> [] then
-            raise (Resolution_error "Input cause is a tautology");
-        res
+  let rec print_cl fmt = function
+    | [] -> Format.fprintf fmt "[]"
+    | [a] -> print_atom fmt a
+    | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a \\/ %a" print_atom a print_cl r
 
-    (* Adding new proven clauses *)
-    let is_proved c = H.mem proof c
-    let is_proven c = is_proved (to_list c)
+  (* Compute resolution of 2 clauses *)
+  let resolve l =
+    let rec aux resolved acc = function
+      | [] -> resolved, acc
+      | [a] -> resolved, a :: acc
+      | a :: b :: r ->
+        if equal_atoms a b then
+          aux resolved (a :: acc) r
+        else if equal_atoms St.(a.neg) b then
+          aux (St.(a.var.pa) :: resolved) acc r
+        else
+          aux resolved (a :: acc) (b :: r)
+    in
+    let resolved, new_clause = aux [] [] l in
+    resolved, List.rev new_clause
 
-    let add_res (c, cl_c) (d, cl_d) =
-        Log.debug 7 "Resolving clauses :";
-        Log.debug 7 "  %a" St.pp_clause c;
-        Log.debug 7 "  %a" St.pp_clause d;
-        let l = List.merge compare_atoms cl_c cl_d in
-        let resolved, new_clause = resolve l in
-        match resolved with
-        | [] -> raise (Resolution_error "No literal to resolve over")
-        | [a] ->
-                H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
-                let new_c = St.make_clause (St.fresh_name ()) new_clause (List.length new_clause) true [c; d] in
-                Log.debug 5 "New clause : %a" St.pp_clause new_c;
-                new_c, new_clause
-        | _ -> raise (Resolution_error "Resolved to a tautology")
+  let to_list c =
+    let v = St.(c.atoms) in
+    let l = ref [] in
+    for i = 0 to Vec.size v - 1 do
+      l := (Vec.get v i) :: !l
+    done;
+    let l, res = resolve (List.sort_uniq compare_atoms !l) in
+    if l <> [] then
+      raise (Resolution_error "Input cause is a tautology");
+    res
 
-    let add_clause cl l = (* We assume that all clauses in c.cpremise are already proved ! *)
-        match l with
-        | a :: ((_ :: _) as r) ->
-                let new_c, new_cl = List.fold_left add_res a r in
-                assert (equal_cl cl new_cl)
-        | _ -> assert false
+  (* Adding new proven clauses *)
+  let is_proved c = H.mem proof c
+  let is_proven c = is_proved (to_list c)
 
-    let need_clause (c, cl) =
-        if is_proved cl then
-            []
-        else if not St.(c.learnt) then begin
-            Log.debug 8 "Adding to hyps : %a" St.pp_clause c;
-            H.add proof cl Assumption;
-            []
+  let add_res (c, cl_c) (d, cl_d) =
+    Log.debug 7 "Resolving clauses :";
+    Log.debug 7 "  %a" St.pp_clause c;
+    Log.debug 7 "  %a" St.pp_clause d;
+    let l = List.merge compare_atoms cl_c cl_d in
+    let resolved, new_clause = resolve l in
+    match resolved with
+    | [] -> raise (Resolution_error "No literal to resolve over")
+    | [a] ->
+      H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d)));
+      let new_c = St.make_clause (St.fresh_name ()) new_clause (List.length new_clause) true [c; d] in
+      Log.debug 5 "New clause : %a" St.pp_clause new_c;
+      new_c, new_clause
+    | _ -> raise (Resolution_error "Resolved to a tautology")
+
+  let add_clause cl l = (* We assume that all clauses in c.cpremise are already proved ! *)
+    match l with
+    | a :: ((_ :: _) as r) ->
+      let new_c, new_cl = List.fold_left add_res a r in
+      if not (equal_cl cl new_cl) then begin
+        Log.debug 0 "Expected the following clauses to be equal :";
+        Log.debug 0 "expected : %s" (Log.on_fmt print_cl cl);
+        Log.debug 0 "found : %a" St.pp_clause new_c;
+        assert false
+      end
+    | _ -> assert false
+
+  let need_clause (c, cl) =
+    if is_proved cl then
+      []
+    else if not St.(c.learnt) then begin
+      Log.debug 8 "Adding to hyps : %a" St.pp_clause c;
+      H.add proof cl Assumption;
+      []
+    end else
+      St.(c.cpremise)
+
+  let rec do_clause = function
+    | [] -> ()
+    | c :: r ->
+      let cl = to_list c in
+      let l = need_clause (c, cl) in
+      if l = [] then (* c is either an asusmption, or already proved *)
+        do_clause r
+      else
+        let l' = List.rev_map (fun c -> c, to_list c) l in
+        let to_prove = List.filter (fun (_, cl) -> not (is_proved cl)) l' in
+        let to_prove = List.rev_map fst to_prove in
+        if to_prove = [] then begin
+          (* See wether we can prove c right now *)
+          add_clause cl l';
+          do_clause r
         end else
-            St.(c.cpremise)
+          (* Or if we have to prove some other clauses first *)
+          do_clause (to_prove @ (c :: r))
 
-    let rec do_clause = function
-        | [] -> ()
-        | c :: r ->
-                let cl = to_list c in
-                let l = need_clause (c, cl) in
-                if l = [] then (* c is either an asusmption, or already proved *)
-                    do_clause r
-                else
-                    let l' = List.rev_map (fun c -> c, to_list c) l in
-                    let to_prove = List.filter (fun (_, cl) -> not (is_proved cl)) l' in
-                    let to_prove = List.rev_map fst to_prove in
-                    if to_prove = [] then begin
-                        (* See wether we can prove c right now *)
-                        add_clause cl l';
-                        do_clause r
-                    end else
-                        (* Or if we have to prove some other clauses first *)
-                        do_clause (to_prove @ (c :: r))
+  let prove c =
+    Log.debug 3 "Proving : %a" St.pp_clause c;
+    do_clause [c];
+    Log.debug 3 "Proved : %a" St.pp_clause c
 
-    let prove c =
-        Log.debug 3 "Proving : %a" St.pp_clause c;
-        do_clause [c];
-        Log.debug 3 "Proved : %a" St.pp_clause c
-
-    let clause_unit a = St.(
-        let l = if a.is_true then [a] else [a.neg] in
-        make_clause (fresh_name ()) l 1 true a.var.vpremise
+  let clause_unit a = St.(
+      let l = if a.is_true then [a] else [a.neg] in
+      make_clause (fresh_name ()) l 1 true a.var.vpremise
     )
 
-    let rec prove_unsat_cl (c, cl) = match cl with
-        | [] -> true
-        | a :: r ->
-                try
-                    Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
-                    let d = match St.(a.var.level, a.var.reason) with
-                    | 0, Some d -> d
-                    | 0, None -> clause_unit a
-                    | _ -> raise Exit
-                    in
-                    prove d;
-                    let cl_d = to_list d in
-                    prove_unsat_cl (add_res (c, cl) (d, cl_d))
-                with Exit -> false
-
-    exception Cannot
-    let assert_can_prove_unsat c =
-        Log.debug 1 "=================== Proof =====================";
-        prove c;
-        if not (prove_unsat_cl (c, to_list c)) then raise Cannot
-
-    (* Interface exposed *)
-    type proof_node = {
-        conclusion : clause;
-        step : step;
-    }
-    and proof = unit -> proof_node
-    and step =
-        | Hypothesis
-        | Lemma of lemma
-        | Resolution of proof * proof * atom
-
-    let rec return_proof (c, cl) () =
-        Log.debug 8 "Returning proof for : %a" St.pp_clause c;
-        let st = match H.find proof cl with
-            | Assumption -> Hypothesis
-            | Lemma l -> Lemma l
-            | Resolution (a, cl_c, cl_d) ->
-                    Resolution (return_proof cl_c, return_proof cl_d, a)
+  let rec prove_unsat_cl (c, cl) = match cl with
+    | [] -> true
+    | a :: r ->
+      try
+        Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c;
+        let d = match St.(a.var.level, a.var.reason) with
+          | 0, Some d -> d
+          | 0, None -> clause_unit a
+          | _ -> raise Exit
         in
-        { conclusion = c; step = st }
+        prove d;
+        let cl_d = to_list d in
+        prove_unsat_cl (add_res (c, cl) (d, cl_d))
+      with Exit -> false
 
-    let prove_unsat c =
-        assert_can_prove_unsat c;
-        return_proof (St.empty_clause, [])
+  exception Cannot
+  let assert_can_prove_unsat c =
+    Log.debug 1 "=================== Proof =====================";
+    prove c;
+    if not (prove_unsat_cl (c, to_list c)) then raise Cannot
 
-    (* Print proof graph *)
-    let _i = ref 0
-    let new_id () = incr _i; "id_" ^ (string_of_int !_i)
+  (* Interface exposed *)
+  type proof_node = {
+    conclusion : clause;
+    step : step;
+  }
+  and proof = unit -> proof_node
+  and step =
+    | Hypothesis
+    | Lemma of lemma
+    | Resolution of proof * proof * atom
 
-    let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;;
-    let c_id c =
-        try
-            snd (Hashtbl.find ids c)
-        with Not_found ->
-            let id = new_id () in
-            Hashtbl.add ids c (false, id);
-            id
+  let rec return_proof (c, cl) () =
+    Log.debug 8 "Returning proof for : %a" St.pp_clause c;
+    let st = match H.find proof cl with
+      | Assumption -> Hypothesis
+      | Lemma l -> Lemma l
+      | Resolution (a, cl_c, cl_d) ->
+        Resolution (return_proof cl_c, return_proof cl_d, a)
+    in
+    { conclusion = c; step = st }
 
-    let clear_ids () =
-        Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids
+  let prove_unsat c =
+    assert_can_prove_unsat c;
+    return_proof (St.empty_clause, [])
 
-    let is_drawn c =
-        try
-            fst (Hashtbl.find ids c)
-        with Not_found ->
-            false
+  (* Print proof graph *)
+  let _i = ref 0
+  let new_id () = incr _i; "id_" ^ (string_of_int !_i)
 
-    let has_drawn c =
-        assert (Hashtbl.mem ids c);
-        let b, id = Hashtbl.find ids c in
-        assert (not b);
-        Hashtbl.replace ids c (true, id)
+  let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;;
+  let c_id c =
+    try
+      snd (Hashtbl.find ids c)
+    with Not_found ->
+      let id = new_id () in
+      Hashtbl.add ids c (false, id);
+      id
 
-    let print_atom fmt a =
-        Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1)
+  let clear_ids () =
+    Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids
 
-    let rec print_cl fmt = function
-        | [] -> Format.fprintf fmt "[]"
-        | [a] -> print_atom fmt a
-        | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a \\/ %a" print_atom a print_cl r
+  let is_drawn c =
+    try
+      fst (Hashtbl.find ids c)
+    with Not_found ->
+      false
 
-    let print_clause fmt c = print_cl fmt (to_list c)
+  let has_drawn c =
+    assert (Hashtbl.mem ids c);
+    let b, id = Hashtbl.find ids c in
+    assert (not b);
+    Hashtbl.replace ids c (true, id)
 
-    let print_dot_rule f arg fmt cl =
-        Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s>%a</TABLE>>];@\n"
-            (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" f arg
+  let print_clause fmt c = print_cl fmt (to_list c)
 
-    let print_dot_edge c fmt d =
-        Format.fprintf fmt "%s -> %s;@\n" (c_id c) (c_id d)
+  let print_dot_rule f arg fmt cl =
+    Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s>%a</TABLE>>];@\n"
+      (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" f arg
 
-    let rec print_dot_proof fmt p =
-        match p.step with
-        | Hypothesis ->
-                let aux fmt () =
-                    Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR>"
-                    print_clause p.conclusion
-                in
-                print_dot_rule aux () fmt p.conclusion
-        | Lemma _ ->
-                let aux fmt () =
-                    Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR><TR><TD>to prove ...</TD></TR>"
-                    print_clause p.conclusion
-                in
-                print_dot_rule aux () fmt p.conclusion
-        | Resolution (proof1, proof2, a) ->
-                let aux fmt () =
-                    Format.fprintf fmt "<TR><TD>%a</TD></TR><TR><TD>%a</TD></TR>"
-                        print_clause p.conclusion print_atom a
-                in
-                let p1 = proof1 () in
-                let p2 = proof2 () in
-                Format.fprintf fmt "%a%a%a%a%a"
-                    (print_dot_rule aux ()) p.conclusion
-                    (print_dot_edge p.conclusion) p1.conclusion
-                    (print_dot_edge p.conclusion) p2.conclusion
-                    print_dot_proof p1
-                    print_dot_proof p2
+  let print_dot_edge c fmt d =
+    Format.fprintf fmt "%s -> %s;@\n" (c_id c) (c_id d)
 
-    let print_dot fmt proof =
-        clear_ids ();
-        Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ())
+  let rec print_dot_proof fmt p =
+    match p.step with
+    | Hypothesis ->
+      let aux fmt () =
+        Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR>"
+          print_clause p.conclusion
+      in
+      print_dot_rule aux () fmt p.conclusion
+    | Lemma _ ->
+      let aux fmt () =
+        Format.fprintf fmt "<TR><TD BGCOLOR=\"LIGHTBLUE\">%a</TD></TR><TR><TD>to prove ...</TD></TR>"
+          print_clause p.conclusion
+      in
+      print_dot_rule aux () fmt p.conclusion
+    | Resolution (proof1, proof2, a) ->
+      let aux fmt () =
+        Format.fprintf fmt "<TR><TD>%a</TD></TR><TR><TD>%a</TD></TR>"
+          print_clause p.conclusion print_atom a
+      in
+      let p1 = proof1 () in
+      let p2 = proof2 () in
+      Format.fprintf fmt "%a%a%a%a%a"
+        (print_dot_rule aux ()) p.conclusion
+        (print_dot_edge p.conclusion) p1.conclusion
+        (print_dot_edge p.conclusion) p2.conclusion
+        print_dot_proof p1
+        print_dot_proof p2
+
+  let print_dot fmt proof =
+    clear_ids ();
+    Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ())
 
 end
 
diff --git a/sat/res_intf.ml b/sat/res_intf.ml
index 4f245ee9..31085929 100644
--- a/sat/res_intf.ml
+++ b/sat/res_intf.ml
@@ -15,8 +15,8 @@ module type S = sig
       @raise Cannot if it is impossible. *)
 
   type proof_node = {
-      conclusion : clause;
-      step : step;
+    conclusion : clause;
+    step : step;
   }
   and proof = unit -> proof_node
   and step =
diff --git a/sat/sat.ml b/sat/sat.ml
index ec73246d..707ce520 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -120,9 +120,9 @@ module Make(Dummy : sig end) = struct
   let eval = SatSolver.eval
 
   let get_proof () =
-      match SatSolver.unsat_conflict () with
-      | None -> assert false
-      | Some c -> SatSolver.Proof.prove_unsat c
+    match SatSolver.unsat_conflict () with
+    | None -> assert false
+    | Some c -> SatSolver.Proof.prove_unsat c
 
   let print_proof = SatSolver.Proof.print_dot
 
diff --git a/sat/solver.mli b/sat/solver.mli
index ea651928..f49d201f 100644
--- a/sat/solver.mli
+++ b/sat/solver.mli
@@ -23,8 +23,8 @@ sig
 
   module Proof : Res.S with
     type atom = St.atom and
-    type clause = St.clause and
-    type lemma = Th.proof
+  type clause = St.clause and
+  type lemma = Th.proof
 
   val solve : unit -> unit
   (** Try and solves the current set of assumptions.
diff --git a/sat/solver_types.ml b/sat/solver_types.ml
index 0a8c5412..103a2f24 100644
--- a/sat/solver_types.ml
+++ b/sat/solver_types.ml
@@ -123,9 +123,9 @@ module Make (F : Formula_intf.S) = struct
         var, negated
 
   let made_vars_info vars =
-      Vec.grow_to_by_double vars !cpt_mk_var;
-      MA.iter (fun _ var -> Vec.set_unsafe vars var.vid var) !ma;
-      !cpt_mk_var
+    Vec.grow_to_by_double vars !cpt_mk_var;
+    MA.iter (fun _ var -> Vec.set_unsafe vars var.vid var) !ma;
+    !cpt_mk_var
 
   let add_atom lit =
     let var, negated = make_var lit in
diff --git a/util/parser.ml b/util/parser.ml
index 0098703e..cde0f4cf 100644
--- a/util/parser.ml
+++ b/util/parser.ml
@@ -15,12 +15,12 @@ type line =
 let rec _read_word s acc i len =
   assert (len>0);
   if i+len=String.length s
-    then String.sub s i len :: acc
-    else match s.[i+len] with
-      | ' ' | '\t' ->
-          let acc = String.sub s i len :: acc in
-          _skip_space s acc (i+len+1)
-      | _ -> _read_word s acc i (len+1)
+  then String.sub s i len :: acc
+  else match s.[i+len] with
+    | ' ' | '\t' ->
+      let acc = String.sub s i len :: acc in
+      _skip_space s acc (i+len+1)
+    | _ -> _read_word s acc i (len+1)
 and _skip_space s acc i =
   if i=String.length s
   then acc
diff --git a/util/sat_solve.ml b/util/sat_solve.ml
index 1d9af7b4..9f7fee14 100644
--- a/util/sat_solve.ml
+++ b/util/sat_solve.ml
@@ -35,26 +35,26 @@ let int_arg r arg =
 
 let setup_gc_stat () =
   at_exit (fun () ->
-    Gc.print_stat stdout;
-  )
+      Gc.print_stat stdout;
+    )
 
 let input_file = fun s -> file := s
 let usage = "Usage : main [options] <file>"
 let argspec = Arg.align [
     "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true),
-      " Enable stack traces";
+    " Enable stack traces";
     "-gc", Arg.Unit setup_gc_stat,
-      " Outputs statistics about the GC";
+    " Outputs statistics about the GC";
     "-model", Arg.Set p_assign,
-      " Outputs the boolean model found if sat";
+    " Outputs the boolean model found if sat";
     "-p", Arg.Set p_proof,
-      " Outputs the proof found (in dot format) if unsat";
+    " Outputs the proof found (in dot format) if unsat";
     "-s", Arg.String (int_arg size_limit),
-      "<s>[kMGT] Sets the size limit for the sat solver";
+    "<s>[kMGT] Sets the size limit for the sat solver";
     "-t", Arg.String (int_arg time_limit),
-      "<t>[smhd] Sets the time limit for the sat solver";
+    "<t>[smhd] Sets the time limit for the sat solver";
     "-v", Arg.Int (fun i -> Log.set_debug i),
-      "<lvl> Sets the debug verbose level";
+    "<lvl> Sets the debug verbose level";
   ]
 
 (* Limits alarm *)
@@ -109,8 +109,8 @@ let main () =
   | S.Unsat ->
     Format.printf "Unsat@.";
     if !p_proof then begin
-        let p = S.get_proof () in
-        S.print_proof Format.std_formatter p
+      let p = S.get_proof () in
+      S.print_proof Format.std_formatter p
     end
 
 let () =
diff --git a/util/sparse_vec.ml b/util/sparse_vec.ml
index 35f20fca..d6054011 100644
--- a/util/sparse_vec.ml
+++ b/util/sparse_vec.ml
@@ -8,7 +8,7 @@ Copyright 2014 Simon Cruanes
 (** {1 Sparse vector, filled with default value} *)
 
 let _size_too_big()=
-    failwith "Sparse_vec: capacity exceeds maximum array size"
+  failwith "Sparse_vec: capacity exceeds maximum array size"
 
 type 'a t = { default : 'a; mutable data : 'a array; mutable sz : int }
 
@@ -17,8 +17,8 @@ let make sz default =
   { default; sz; data=Array.make sz default; }
 
 let init sz f default =
-    if sz > Sys.max_array_length then _size_too_big();
-    {data = Array.init sz (fun i -> f i); sz ; default}
+  if sz > Sys.max_array_length then _size_too_big();
+  {data = Array.init sz (fun i -> f i); sz ; default}
 
 let length {sz} = sz
 
@@ -37,7 +37,7 @@ let rec grow_to_by_double t new_capa =
   let data = t.data in
   let capa = ref (Array.length data + 1) in
   while !capa < new_capa do
-      capa := min (2 * !capa) Sys.max_array_length;
+    capa := min (2 * !capa) Sys.max_array_length;
   done;
   grow_to t !capa
 
diff --git a/util/vec.ml b/util/vec.ml
index 7930216e..29aa6e1d 100644
--- a/util/vec.ml
+++ b/util/vec.ml
@@ -14,17 +14,17 @@
 type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int }
 
 let _size_too_big()=
-    failwith "Vec: capacity exceeds maximum array size"
+  failwith "Vec: capacity exceeds maximum array size"
 
 let make capa d =
-    if capa > Sys.max_array_length then _size_too_big();
-    {data = Array.make capa d; sz = 0; dummy = d}
+  if capa > Sys.max_array_length then _size_too_big();
+  {data = Array.make capa d; sz = 0; dummy = d}
 
 let make_empty d = {data = [||]; sz=0; dummy=d }
 
 let init capa f d =
-    if capa > Sys.max_array_length then _size_too_big();
-    {data = Array.init capa (fun i -> f i); sz = capa; dummy = d}
+  if capa > Sys.max_array_length then _size_too_big();
+  {data = Array.init capa (fun i -> f i); sz = capa; dummy = d}
 
 let from_array data sz d =
   assert (sz <= Array.length data);
@@ -53,16 +53,16 @@ let grow_to t new_capa =
   t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy)
 
 let grow_to_double_size t =
-    if Array.length t.data = Sys.max_array_length then _size_too_big();
-    let size = min Sys.max_array_length (2* Array.length t.data) in
-    grow_to t size
+  if Array.length t.data = Sys.max_array_length then _size_too_big();
+  let size = min Sys.max_array_length (2* Array.length t.data) in
+  grow_to t size
 
 let rec grow_to_by_double t new_capa =
   if new_capa > Sys.max_array_length then _size_too_big ();
   let data = t.data in
   let capa = ref (Array.length data + 1) in
   while !capa < new_capa do
-      capa := min (2 * !capa) Sys.max_array_length;
+    capa := min (2 * !capa) Sys.max_array_length;
   done;
   grow_to t !capa