diff --git a/src/cli/lambdapi.ml b/src/cli/lambdapi.ml
index efc5fb874..e53b1cfae 100644
--- a/src/cli/lambdapi.ml
+++ b/src/cli/lambdapi.ml
@@ -233,7 +233,7 @@ let output : output option CLT.t =
       match s with
       | "lp" -> Ok Lp
       | "dk" -> Ok Dk
-      | "hrs" -> Ok Hrs      
+      | "hrs" -> Ok Hrs
       | "xtc" -> Ok Xtc
       | "afsm" -> Ok Afsm
       | "trs" -> Ok Trs
diff --git a/src/export/afsm.ml b/src/export/afsm.ml
index c63c4d663..016e9ec9a 100644
--- a/src/export/afsm.ml
+++ b/src/export/afsm.ml
@@ -1,13 +1,13 @@
-(** This module provides a function to translate a signature to the AFSM format
-   used by the Wanda termination checker. Note that because termination is 
-   checked at the untyped level, Wanda will *always* answer NO, as we have an 
-   untyped beta rule. However, by removing the beta rule we can sometimes show 
-   termination of the rest of the system. This can be useful when showing 
-   confluence of the system: by Von Oostrom's orthogonal combinations 
-   criterion, if the system without beta is confluent, then by combining it
-   with beta it stays confluent. Thus, if the system without beta is weakly 
-   confluent, then by checking its termination we can deduce the confluence
-   of the system with beta.
+(** This module provides a function to translate a signature to the AFSM
+   format used by the Wanda termination checker. Note that because
+   termination is checked at the untyped level, Wanda will *always* answer NO,
+   as we have an untyped beta rule. However, by removing the beta rule we can
+   sometimes show termination of the rest of the system. This can be useful
+   when showing confluence of the system: by Von Oostrom's orthogonal
+   combinations criterion, if the system without beta is confluent, then by
+   combining it with beta it stays confluent. Thus, if the system without beta
+   is weakly confluent, then by checking its termination we can deduce the
+   confluence of the system with beta.
 
 - Lambdapi terms are translated to terms over the following base signature:
 
@@ -28,16 +28,16 @@ Pattern variables of arity n are translated as variables of type t -> ... -> t
    names. So bound variables are translated into positive integers and pattern
    variables are translated as XiNj where i is the number of the rule and j
    is the indice of the variable. Function symbols are translated directly
-   by their unqualified names. If a function symbol name clashes with the 
-   name of a variable, metavariable or a symbol declared in the base 
-   signature, we prefix it with !. In order to do this, we assume that no 
+   by their unqualified names. If a function symbol name clashes with the
+   name of a variable, metavariable or a symbol declared in the base
+   signature, we prefix it with !. In order to do this, we assume that no
    function symbol starts with !.
 
 - Unicode is translated as unicode, and Wanda does not accept it. We chose not
-   to implement a translation to their codes, as the output would be unreadable. 
-   In this case, it is better if the user removes manually the unicode from their
-   file, this way they can chose a more readable replacement for the occuring
-   unicode characters.
+   to implement a translation to their codes, as the output would be
+   unreadable. In this case, it is better if the user removes manually the
+   unicode from their file, this way they can chose a more readable
+   replacement for the occuring unicode characters.
  *)
 
 open Lplib open Base open Extra
@@ -49,19 +49,19 @@ let syms = ref SymMap.empty
 (** [nb_rules] is the number of rewrite rules. *)
 let nb_rules = ref 0
 
-let sanitize_name : string -> string = fun s -> 
+let sanitize_name : string -> string = fun s ->
   (* we considere names starting with '!' as forbiden, so we can
      use it as an escape character to prevent clashes *)
   if s.[0] = '!' then assert false;
-  match s with   
-  | "A" | "L" | "P" | "B" -> 
+  match s with
+  | "A" | "L" | "P" | "B" ->
     (* prevents clashes with the names in the base signature *)
-    "!" ^ s 
-  | _ -> 
+    "!" ^ s
+  | _ ->
     (* prevent clashes metavariable names *)
-    if s.[0] = 'X' then "!" ^ s 
+    if s.[0] = 'X' then "!" ^ s
     (* prevent clashes with variable names, which are just numbers *)
-    else if Str.string_match (Str.regexp "[0-9]+$") s 0 then "!" ^ s  
+    else if Str.string_match (Str.regexp "[0-9]+$") s 0 then "!" ^ s
     else s (* ok names *)
 
 (** [sym_name s] translates the symbol name of [s]. *)
@@ -109,7 +109,7 @@ let rec term : term pp = fun ppf t ->
   | LLet(a,t,b) ->
     let x, b = Bindlib.unbind b in
     out ppf "B %a %a (/\\%a.%a)" term_safe a term_safe t bvar x term b
-and term_safe : term pp = fun ppf t -> 
+and term_safe : term pp = fun ppf t ->
   match unfold t with
   | Vari v -> bvar ppf v
   | Symb s -> add_sym s; sym ppf s
@@ -117,7 +117,7 @@ and term_safe : term pp = fun ppf t ->
   | Patt(Some i,_,ts) ->
     let k = Array.length ts in
     let args ppf ts = for i=1 to k-1 do out ppf ",%a" term ts.(i) done in
-    out ppf "%a[%a%a]" pvar i term ts.(0) args ts  
+    out ppf "%a[%a%a]" pvar i term ts.(0) args ts
   | _ -> out ppf "(%a)" term t
 
 (** [rule ppf r] translates the pair of terms [r] as a rule. *)
@@ -152,7 +152,7 @@ let sign : Sign.t pp = fun ppf sign ->
   let pp_syms : string SymMap.t pp = fun ppf syms ->
     let sym_decl : string pp = fun ppf n -> out ppf "\n%s : t" n in
     let sym_decl _ n = sym_decl ppf n in SymMap.iter sym_decl syms
-  in    
+  in
   out ppf "\
 A : t -> t -> t
 L : t -> (t -> t) -> t
diff --git a/src/export/trs.ml b/src/export/trs.ml
index 70f2ac19d..ba482b2a0 100644
--- a/src/export/trs.ml
+++ b/src/export/trs.ml
@@ -2,10 +2,10 @@
    used in the confluence competition.
 
    This translation relies on the following fact: if in all rules l --> r of
-   the rewrite system both l and r are patterns, then the system is SN whenever
-   the first-order system obtained by forgeting about binders also termintes.
-   Note that because of this, we consider only termination without the beta 
-   rule, as its right hand side is not a pattern.    
+   the rewrite system both l and r are patterns, then the system is SN
+   whenever the first-order system obtained by forgeting about binders also
+   termintes. Note that because of this, we consider only termination without
+   the beta rule, as its right hand side is not a pattern.
 
 - Lambdapi terms are translated to a TRS over the following base signature:
 
@@ -17,33 +17,33 @@
 
   P // binary symbol for Π
 
-- Function symbols are translated directly by their unqualified names. If a 
+- Function symbols are translated directly by their unqualified names. If a
    function symbol name clashes with the name of a variable, metavariable or
    a symbol declared in the base signature, we prefix it with !. In order to
    do this, we assume that no function symbol starts with !.
 
-TODO: 
+TODO:
+
+- For the time being, we translate rules without verifying that the pattern
+   condition is always verified. In the future we should only translate the
+   fragment of the system that satisfy the pattern confition in both the lhs
+   and the rhs.
 
-- For the time being, we translate rules without verifying that the pattern 
-   condition is always verified. In the future we should only translate the 
-   fragment of the system that satisfy the pattern confition in both the lhs 
-   and the rhs. 
-   
 *)
 
 open Lplib open Base open Extra
 open Core open Term
 
-let sanitize_name : string -> string = fun s -> 
+let sanitize_name : string -> string = fun s ->
   (* we considere names starting with '!' as forbiden, so we can
      use it as an escape character to prevent clashes *)
   if s.[0] = '!' then assert false;
-  match s with   
-  | "A" | "L" | "P" | "B" -> 
+  match s with
+  | "A" | "L" | "P" | "B" ->
     (* prevents clashes with the names in the base signature *)
-    "!" ^ s 
+    "!" ^ s
   | _ -> s
-  
+
 (** [sym_name s] translates the symbol name of [s]. *)
 let sym_name : sym pp = fun ppf s ->
     out ppf "%s" (sanitize_name s.sym_name)
@@ -71,7 +71,7 @@ let rec term : term pp = fun ppf t ->
   | Patt(None,_,_) -> assert false
   | Patt(Some i,_,[||]) -> set_max_var i; pvar ppf i
   | Patt(Some i,_,_) -> (* todo: check it's only applied to bound vars*)
-    set_max_var i; pvar ppf i 
+    set_max_var i; pvar ppf i
   | Appl(t,u) -> out ppf "A(%a, %a)" term t term u
   | Abst(a,b) ->
     let _, b = Bindlib.unbind b in
@@ -81,7 +81,7 @@ let rec term : term pp = fun ppf t ->
     out ppf "P(%a, %a)" term a  term b
   | LLet(a,t,b) ->
     let _, b = Bindlib.unbind b in
-    out ppf "B(%a,%a,%a)" term a term t  term b
+    out ppf "B(%a,%a,%a)" term a term t term b
 
 (** [rule ppf r] translates the pair of terms [r] as a rule. *)
 let rule : (term * term) pp = fun ppf (l, r) ->
@@ -110,8 +110,8 @@ let sign : Sign.t pp = fun ppf sign ->
   let ppf_rules = Format.formatter_of_buffer buf_rules in
   Sign.iterate (rules_of_sign ppf_rules) sign;
   Format.pp_print_flush ppf_rules ();
-  let pp_vars : int pp = fun ppf k -> 
-    for i = 0 to k do out ppf " $%d" i done in  
+  let pp_vars : int pp = fun ppf k ->
+    for i = 0 to k do out ppf " $%d" i done in
   out ppf "\
 (VAR%a)
 (RULES