diff --git a/src/core/trans.ml b/src/core/trans.ml
index a64397f2462d8f0575ddeb48f1ee5cdd872f04d2..2f3fbf81e052b30d190dff2df9269a8c6f168048 100644
--- a/src/core/trans.ml
+++ b/src/core/trans.ml
@@ -118,15 +118,13 @@ let notImplemented s = error (NotImplemented s)
 
 let report fmt = function
   | UnsupportedExpression (e,s) ->
+      let msg = "The transformation doesn't support this expression" in
       Format.fprintf fmt
-        "@[<hov 3> The transformation doesn't support this expression :@\n\
-%a@\n\
-%s@]@\n" Pretty.print_expr e s
+        "@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_expr e s
   | UnsupportedDeclaration (d,s) ->
+      let msg = "The transformation doesn't support this declaration" in
       Format.fprintf fmt
-        "@[<hov 3> The transformation doesn't support this declaration :@\n\
-%a@\n\
-%s@]@\n" Pretty.print_decl d s
+        "@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_decl d s
   | NotImplemented (s) ->
-      Format.fprintf fmt
-        "@[<hov 3> Unimplemented features :@\n%s@]@\n" s
+      Format.fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]@\n" s
+
diff --git a/src/core/trans.mli b/src/core/trans.mli
index 8bba8548a0a080f8a607c63faebc42b1d4008233..2051b53e714b31cb8f2da9c6e0921ef13be0dd30 100644
--- a/src/core/trans.mli
+++ b/src/core/trans.mli
@@ -57,10 +57,8 @@ val decl_l : (decl -> decl list list) -> task -> task tlist
 
 val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
 
-
 (** exception to use in a transformation *)
 
-
 type error =
   | UnsupportedExpression of expr * string
   | UnsupportedDeclaration of decl * string
@@ -70,7 +68,7 @@ exception Error of error
 
 val unsupportedExpression : expr -> string -> 'a
 val unsupportedDeclaration : decl -> string -> 'a
-(** - [expr] is the problematic formula 
+(** - [expr] is the problematic formula
     - [string] explain the problem and
       possibly a way to solve it (such as applying another
       transforamtion) *)
@@ -78,5 +76,5 @@ val unsupportedDeclaration : decl -> string -> 'a
 val notImplemented : string -> 'a
 (** [string] explain what is not implemented *)
 
-
 val report : Format.formatter -> error -> unit
+
diff --git a/src/transform/eliminate_inductive.ml b/src/transform/eliminate_inductive.ml
index 20080ab6461af80bfea3e18e772bf4a01f0d18e7..f320cb8f8c32a72c82c7de6af69a3f0e6ca84099 100644
--- a/src/transform/eliminate_inductive.ml
+++ b/src/transform/eliminate_inductive.ml
@@ -36,7 +36,7 @@ let exi vl (_,f) =
     | Fapp (_,tl) ->
         let marry acc v t = f_and_simp acc (f_equ v t) in
         List.fold_left2 marry f_true vl tl
-    | _ -> Trans.unsupportedExpression (Fmla f) "eliminate_inductive"
+    | _ -> assert false
   in
   descend f