8 files changed, 17 insertions, 23 deletions
diff --git a/testsuite/tests/misc-kb/equations.ml b/testsuite/tests/misc-kb/equations.ml
index 5617bc4f9d..1d905e015d 100644
--- a/testsuite/tests/misc-kb/equations.ml
+++ b/testsuite/tests/misc-kb/equations.ml
@@ -16,7 +16,7 @@
 
 open Terms
 
-type rule = 
+type rule =
   { number: int;
     numvars: int;
     lhs: term;
@@ -53,7 +53,7 @@ let pretty_rule rule =
 
 
 let pretty_rules rules = List.iter pretty_rule rules
- 
+
 (****************** Rewriting **************************)
 
 (* Top-level rewriting. Let eq:L=R be an equation, M be a term such that L<=M.
@@ -112,4 +112,3 @@ let rec mrewrite_all rules m =
     mrewrite_all rules (mrewrite1 rules m)
   with Failure _ ->
     m
-
diff --git a/testsuite/tests/misc-kb/equations.mli b/testsuite/tests/misc-kb/equations.mli
index 0db190b858..49b1a461e7 100644
--- a/testsuite/tests/misc-kb/equations.mli
+++ b/testsuite/tests/misc-kb/equations.mli
@@ -14,7 +14,7 @@
 
 open Terms
 
-type rule = 
+type rule =
   { number: int;
     numvars: int;
     lhs: term;
diff --git a/testsuite/tests/misc-kb/kb.ml b/testsuite/tests/misc-kb/kb.ml
index ff357b3ff8..5045a31881 100644
--- a/testsuite/tests/misc-kb/kb.ml
+++ b/testsuite/tests/misc-kb/kb.ml
@@ -37,7 +37,7 @@ let rec super m = function
 
 
 (* Ex :
-let (m,_) = <<F(A,B)>> 
+let (m,_) = <<F(A,B)>>
 and (n,_) = <<H(F(A,x),F(x,y))>> in super m n
 ==> [[1],[2,Term ("B",[])];                      x <- B
      [2],[2,Term ("A",[]); 1,Term ("B",[])]]     x <- A  y <- B
@@ -109,7 +109,7 @@ let rec get_rule n = function
 
 (* Improved Knuth-Bendix completion procedure *)
 
-let kb_completion greater = 
+let kb_completion greater =
   let rec kbrec j rules =
   let rec process failures (k,l) eqs =
 (****
@@ -165,7 +165,7 @@ let kb_completion greater =
                   (strict_critical_pairs el (rename rl.numvars el))
         else
           try
-            let rk = get_rule k rules in 
+            let rk = get_rule k rules in
             let ek = (rk.lhs, rk.rhs) in
               process failures (k,l)
                       (mutual_critical_pairs el (rename rl.numvars ek))
@@ -185,4 +185,3 @@ let kb_complete greater complete_rules rules =
       kb_completion greater n complete_rules [] (n,n) eqs in
     print_string "Canonical set found :"; print_newline();
     pretty_rules (List.rev completed_rules)
-
diff --git a/testsuite/tests/misc-kb/kbmain.ml b/testsuite/tests/misc-kb/kbmain.ml
index 580b715040..a0d4ff715b 100644
--- a/testsuite/tests/misc-kb/kbmain.ml
+++ b/testsuite/tests/misc-kb/kbmain.ml
@@ -72,11 +72,10 @@ let group_precedence op1 op2 =
     if r1 = r2 then Equal else
     if r1 > r2 then Greater else NotGE
 
-let group_order = rpo group_precedence lex_ext 
+let group_order = rpo group_precedence lex_ext
 
 let greater pair =
   match group_order pair with Greater -> true | _ -> false
 
 let _ =
   for i = 1 to 20 do kb_complete greater [] geom_rules done
-
diff --git a/testsuite/tests/misc-kb/orderings.ml b/testsuite/tests/misc-kb/orderings.ml
index c81746e309..6da73df8d7 100644
--- a/testsuite/tests/misc-kb/orderings.ml
+++ b/testsuite/tests/misc-kb/orderings.ml
@@ -16,7 +16,7 @@
 
 open Terms
 
-type ordering = 
+type ordering =
     Greater
   | Equal
   | NotGE
@@ -65,10 +65,10 @@ let lex_ext order = function
       | ( _ , []) -> Greater
       | (x1::l1, x2::l2) ->
           match order (x1,x2) with
-            Greater -> if List.for_all (fun n' -> gt_ord order (m,n')) l2 
+            Greater -> if List.for_all (fun n' -> gt_ord order (m,n')) l2
                        then Greater else NotGE
           | Equal -> lexrec (l1,l2)
-          | NotGE -> if List.exists (fun m' -> ge_ord order (m',n)) l1 
+          | NotGE -> if List.exists (fun m' -> ge_ord order (m',n)) l1
                      then Greater else NotGE in
       lexrec (sons1, sons2)
   | _ -> failwith "lex_ext"
@@ -76,9 +76,9 @@ let lex_ext order = function
 
 (* Recursive path ordering *)
 
-let rpo op_order ext = 
+let rpo op_order ext =
   let rec rporec (m,n) =
-    if m = n then Equal else 
+    if m = n then Equal else
       match m with
           Var vm -> NotGE
         | Term(op1,sons1) ->
@@ -96,4 +96,3 @@ let rpo op_order ext =
                         if List.exists (fun m' -> ge_ord rporec (m',n)) sons1
                         then Greater else NotGE
   in rporec
-
diff --git a/testsuite/tests/misc-kb/orderings.mli b/testsuite/tests/misc-kb/orderings.mli
index bb44f0832d..d75c58a029 100644
--- a/testsuite/tests/misc-kb/orderings.mli
+++ b/testsuite/tests/misc-kb/orderings.mli
@@ -14,7 +14,7 @@
 
 open Terms
 
-type ordering = 
+type ordering =
     Greater
   | Equal
   | NotGE
diff --git a/testsuite/tests/misc-kb/terms.ml b/testsuite/tests/misc-kb/terms.ml
index 86604f9c5a..f7a1c3e7b7 100644
--- a/testsuite/tests/misc-kb/terms.ml
+++ b/testsuite/tests/misc-kb/terms.ml
@@ -14,7 +14,7 @@
 
 (****************** Term manipulations *****************)
 
-type term = 
+type term =
     Var of int
   | Term of string * term list
 
@@ -22,7 +22,7 @@ let rec union l1 l2 =
   match l1 with
     []   -> l2
   | a::r -> if List.mem a l2 then union r l2 else a :: union r l2
-  
+
 
 let rec vars = function
     Var n -> [n]
@@ -73,7 +73,7 @@ let matching term1 term2 =
 
 (* A naive unification algorithm. *)
 
-let compsubst subst1 subst2 = 
+let compsubst subst1 subst2 =
   (List.map (fun (v,t) -> (v, substitute subst1 t)) subst2) @ subst1
 
 
@@ -133,5 +133,3 @@ and pretty_close = function
         pretty_term m
   | m ->
       pretty_term m
-
-
diff --git a/testsuite/tests/misc-kb/terms.mli b/testsuite/tests/misc-kb/terms.mli
index 0f6be4c8e8..40c7710818 100644
--- a/testsuite/tests/misc-kb/terms.mli
+++ b/testsuite/tests/misc-kb/terms.mli
@@ -12,7 +12,7 @@
 
 (* $Id$ *)
 
-type term = 
+type term =
     Var of int
   | Term of string * term list