diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 8c062fe0f7069aad60cfd046036d28087226fa19..34b70fff46d4d7dd95dbbd388e57a3ef540c7ecb 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -354,7 +354,7 @@ let queueInsertState state = queueStates := state::!queueStates
 (* original version: breadth-first *)
 let queueInsertCore core = queueCores2 := core::!queueCores2
 
-(* experiment: depth first 
+(* experiment: depth first
 let queueInsertCore core = queueCores1 := core::!queueCores1
 *)
 
@@ -890,15 +890,15 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
         else ();
         let s1 = List.nth sortlst (if first then 0 else 1) in
         detClosure nomTbl hcF fset atset nomset s1 f1
-	(*
+    (*
        FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
-	 *)
-	| C.HCMU (name, f1) ->
-	   let unfold = C.hc_replace hcF name f f1 in
-	   detClosure nomTbl hcF fset atset nomset s unfold
-	| C.HCNU (name, f1) ->
-	   let unfold = C.hc_replace hcF name f f1 in
-	   detClosure nomTbl hcF fset atset nomset s unfold
+     *)
+    | C.HCMU (name, f1) ->
+       let unfold = C.hc_replace hcF name f f1 in
+       detClosure nomTbl hcF fset atset nomset s unfold
+    | C.HCNU (name, f1) ->
+       let unfold = C.hc_replace hcF name f f1 in
+       detClosure nomTbl hcF fset atset nomset s unfold
 
 
 let detClosureAt hcF atset name f () =
@@ -909,7 +909,7 @@ let detClosureAt hcF atset name f () =
   | C.HCAND _
   | C.HCAT _ -> ()
   | _ ->
-      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in 
+      let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
       C.HcFHt.replace atset at ()
 
 (** Initialises the arrays for a formula and its integer representation.
@@ -945,10 +945,10 @@ let initTables nomTbl hcF htF htR s f n =
       !arrayType.(s).(n) <- AndF;
       !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) f1;
       !arrayDest2.(s).(n) <- C.HcFHt.find htF.(s) f2
-  | C.HCEX (role, f1) -> 
+  | C.HCEX (role, f1) ->
       !arrayType.(s).(n) <- ExF;
       !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
-      !arrayDest3.(s).(n) <- 
+      !arrayDest3.(s).(n) <-
         if Hashtbl.mem htR role then Hashtbl.find htR role
         else
           let size = Hashtbl.length htR in
@@ -1030,11 +1030,11 @@ let initTables nomTbl hcF htF htR s f n =
   | C.HCID (f1) ->
       !arrayType.(s).(n) <- IdF;
       !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1
-  | C.HCNORM (f1, f2) ->    
+  | C.HCNORM (f1, f2) ->
       !arrayType.(s).(n) <- NormF;
       !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
       !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
-  | C.HCNORMN (f1, f2) ->    
+  | C.HCNORMN (f1, f2) ->
       !arrayType.(s).(n) <- NormnF;
       !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 0) f1;
       !arrayDest2.(s).(n) <- C.HcFHt.find htF.(List.nth sortlst 1) f2
@@ -1050,12 +1050,12 @@ let initTables nomTbl hcF htF htR s f n =
       !arrayDest3.(s).(n) <- if first then 0 else 1
   | C.HCMU (name, f1) ->
      !arrayType.(s).(n) <- MuF;
-	 let unfold = C.hc_replace hcF name f f1 in
-	 !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
+     let unfold = C.hc_replace hcF name f f1 in
+     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
   | C.HCNU (name, f1) ->
-	 !arrayType.(s).(n) <- NuF;
-	 let unfold = C.hc_replace hcF name f f1 in
-	 !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
+     !arrayType.(s).(n) <- NuF;
+     let unfold = C.hc_replace hcF name f f1 in
+     !arrayDest1.(s).(n) <- C.HcFHt.find htF.(s) unfold
   | C.HCVAR _ -> !arrayType.(s).(n) <- Other
 
 
@@ -1070,7 +1070,7 @@ let initTablesAt hcF htF name sort =
     | C.HCAND _
     | C.HCAT _ -> ()
     | _ ->
-        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in 
+        let at = C.HcFormula.hashcons hcF (C.HCAT (name, f)) in
         let atn = C.HcFHt.find htF.(0) at in
         FHt.add !arrayAt.(sort).(n) nom atn
   in