diff --git a/src/transform/encoding.ml b/src/transform/encoding.ml
index 2393941a4b0c028238396c5429810948fb6aeb38..aa73cecdb55b54347b07683fc4fb7fc06f453547 100644
--- a/src/transform/encoding.ml
+++ b/src/transform/encoding.ml
@@ -64,30 +64,6 @@ let enco_kept = enco_gen kept_opt
 let enco_poly_smt = enco_gen poly_smt_opt
 let enco_poly_tptp = enco_gen poly_tptp_opt
 
-let forbid_for_explicit =
-  Encoding_enumeration.forbid_enumeration
-    "explicit is unsound in presence of this finite type"
-
-let maybe_forbid_enumeration =
-  Trans.on_meta_excl poly_smt_opt.meta (fun alo ->
-    let s = match alo with
-      | None -> poly_smt_opt.default
-      | Some [MAstr s] -> s
-      | _ -> assert false in
-    if s = "explicit"
-    then forbid_for_explicit
-    else Trans.identity)
-
-let forbid_enumeration =
-  Trans.on_meta_excl poly_smt_opt.meta (fun alo ->
-    let s = match alo with
-      | None -> poly_smt_opt.default
-      | Some [MAstr s] -> s
-      | _ -> assert false in
-    if s = "explicit"
-    then forbid_for_explicit
-    else Encoding_enumeration.encoding_enumeration)
-
 
 open Ty
 open Term
@@ -113,15 +89,15 @@ let monomorphise_goal =
 
 let encoding_smt env =
   compose monomorphise_goal
-    (compose maybe_forbid_enumeration
-       (compose (enco_select env)
-          (compose (enco_kept env) (enco_poly_smt env))))
+    (compose (enco_select env)
+       (compose (enco_kept env) (enco_poly_smt env)))
 
 let encoding_tptp env =
   compose monomorphise_goal
-    (compose forbid_enumeration
-       (compose (enco_select env)
-          (compose (enco_kept env) (enco_poly_tptp env))))
+    (compose (enco_select env)
+       (compose (enco_kept env)
+          (compose (enco_poly_tptp env)
+             Encoding_enumeration.encoding_enumeration)))
 
 let () =
   register_env_transform "encoding_smt" encoding_smt;
diff --git a/src/transform/encoding.mli b/src/transform/encoding.mli
index 9e30ceca9b9151508fc01cc29da96e39ff59b26d..dda00e804d11c8943beca34fee956b51a8ff4408 100644
--- a/src/transform/encoding.mli
+++ b/src/transform/encoding.mli
@@ -32,7 +32,6 @@ val register_enco_poly : string -> (env -> task trans) -> unit
 
 
 val monomorphise_goal : Task.task Trans.trans
-val maybe_forbid_enumeration : Task.task Trans.trans
 
 val enco_poly_smt : Env.env -> Task.task Trans.trans
 val print_kept : Task.task Trans.trans
diff --git a/src/transform/encoding_arrays.ml b/src/transform/encoding_arrays.ml
index af629840492bde61b99d523073207cb32d1798ed..0c9823999fb2f0a1dfe1531679c748ec79e95817 100644
--- a/src/transform/encoding_arrays.ml
+++ b/src/transform/encoding_arrays.ml
@@ -576,15 +576,14 @@ let encoding_smt_array env =
   Trans.on_used_theory th_array (fun used ->
     if not used then Encoding.encoding_smt env else
       compose Encoding.monomorphise_goal
-        (compose Encoding.maybe_forbid_enumeration
-           (compose (select_subterm_array th_array)
-              (compose Encoding.print_kept
-                 (compose (Encoding_instantiate.t
-                             (create_env_array env th_array))
-                    (compose meta_arrays_to_meta_kept
-                       (compose Encoding.print_kept
-                          (compose (Encoding_bridge.t env)
-                             (Encoding.enco_poly_smt env)))))))))
+        (compose (select_subterm_array th_array)
+           (compose Encoding.print_kept
+              (compose (Encoding_instantiate.t
+                          (create_env_array env th_array))
+                 (compose meta_arrays_to_meta_kept
+                    (compose Encoding.print_kept
+                       (compose (Encoding_bridge.t env)
+                          (Encoding.enco_poly_smt env))))))))
 
 let () = Trans.register_env_transform "encoding_smt_array" encoding_smt_array
 
diff --git a/src/transform/encoding_enumeration.ml b/src/transform/encoding_enumeration.ml
index b5706f142cd5749e7f544e03546257459e96420a..690e5f283a8e01c2adee83898a8d0f18c7dbafef 100644
--- a/src/transform/encoding_enumeration.ml
+++ b/src/transform/encoding_enumeration.ml
@@ -45,6 +45,8 @@ let proj tenv t ty = match ty.ty_node with
   | Tyapp (ts,_) when Sts.mem ts tenv.enum ->
       let fs = Hts.find tenv.projs ts in
       t_app fs [t] t.t_ty
+  | _ when ty_s_any (fun ts -> Sts.mem ts tenv.enum) t.t_ty ->
+      Printer.unsupportedType ty "complexe finite type"
   | _ -> t
 
 let proj tenv t = match t.t_node with
@@ -93,10 +95,5 @@ let encoding_enumeration =
     let tenv = { enum = enum ; projs = projs } in
     Trans.decl (decl tenv) None)
 
-let forbid_enumeration s =
-  Trans.on_tagged_ts meta_enum (fun enum ->
-    if Sts.is_empty enum then Trans.identity
-    else Printer.unsupportedTysymbol (Sts.choose enum) s)
-
 let () = Trans.register_transform "encoding_enumeration" encoding_enumeration
 
diff --git a/src/transform/encoding_enumeration.mli b/src/transform/encoding_enumeration.mli
index 40281732acfdb3047d14718f096a6ddd9da657d7..bd1ec2ad3c383955bd2c8ab35a378de76eaeaa18 100644
--- a/src/transform/encoding_enumeration.mli
+++ b/src/transform/encoding_enumeration.mli
@@ -18,6 +18,3 @@
 (**************************************************************************)
 
 val encoding_enumeration : Task.task Trans.trans
-val forbid_enumeration   : string ->Task.task Trans.trans
-(* [forbid_enumeration s] if the task contains encoded enumeration
-   unsupportedTysymbol is raised with the message [s] *)
diff --git a/src/transform/encoding_explicit.ml b/src/transform/encoding_explicit.ml
index 8381a892234fe464709f4e358c781329b055493d..726d5c5bd3834757cb465b9d1d9e3b4eb48ea412 100644
--- a/src/transform/encoding_explicit.ml
+++ b/src/transform/encoding_explicit.ml
@@ -38,9 +38,11 @@ module Debug = struct
   (** utility to print a list of items *)
   let rec print_list printer fmter = function
     | [] -> Format.fprintf fmter ""
-    | e::es -> if es = []
-        then Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
-        else Format.fprintf fmter "@[%a@], %a" printer e (print_list printer) es
+    | e::es ->
+      if es = [] then
+        Format.fprintf fmter "@[%a@] %a" printer e (print_list printer) es
+      else
+        Format.fprintf fmter "@[%a@], %a" printer e (print_list printer) es
 
   let debug x = Format.eprintf "%s@." x
 end
@@ -137,6 +139,15 @@ let decl d = match d.d_node with
 
 let explicit = Trans.decl decl (Task.add_decl None d_ts_type)
 
+let meta_enum = Eliminate_algebraic.meta_enum
+
+let explicit =
+  Trans.on_tagged_ts meta_enum (fun enum ->
+    if Sts.is_empty enum then explicit
+    else Printer.unsupportedTysymbol (Sts.choose enum)
+      "explicit is unsound in presence of type")
+
+
 (** {2 monomorphise task } *)
 
 let ts_base = create_tysymbol (id_fresh "uni") [] None