diff --git a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
index 1c41d61..db65c6d 100644
--- a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
+++ b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
@@ -47,19 +47,21 @@ type 'f gen_data =
       decls: ('f, 'f var_spec) decls;
       ltyps: (typ * 'f option) SMap.t;
       qname: string -> qualname;
-      mutable tdefs: type_name SMap.t;
+      typ_symbs: type_name SMap.t;
       mutable env: var_dec Env.t;
       mutable var_names: ident SMap.t;
     }
 
+let no_typ_symbs: type_name SMap.t = SMap.empty
+
 (* --- *)
 
-let mk_gen_data qual decls typdefs =
+let mk_gen_data qualname typ_symbs decls typdefs =
   {
     decls;
     ltyps = label_typs typdefs;
-    qname = (fun name -> { qual; name });
-    tdefs = SMap.empty;
+    qname = (fun name -> { qual = modul qualname; name });
+    typ_symbs;
     env = Env.empty;
     var_names = SMap.empty;
   }
@@ -72,7 +74,7 @@ let translate_typ gd vdecl = function
   | `Bool -> Initial.tbool
   | `Int -> Initial.tint
   | `Real -> Initial.tfloat
-  | `Enum tn -> Tid (SMap.find tn gd.tdefs)
+  | `Enum tn -> Tid (SMap.find tn gd.typ_symbs)
   | t -> raise (Untranslatable (asprintf "type %a" print_typ t,
                                opt_decl_loc gd vdecl))
 
@@ -81,8 +83,6 @@ let symb_typ gd s = try match SMap.find s gd.decls with | typ, _, _ -> typ with
 
 let symb_typ' gd s = translate_typ gd s (symb_typ gd s)
 
-let translate_label gd l = gd.qname (Symb.to_string (label_symb l))
-
 let ts gd v = try SMap.find v gd.var_names with Not_found ->
   failwith (asprintf "Variable name `%a' unavailable; \
                       was it an output of the main node?" Symb.print v)
@@ -241,56 +241,59 @@ let translate_expr gd e =
 
 (* --- *)
 
-(* let decl_typs typdefs gd = *)
-(*   fold_typdefs begin fun tname tdef typs -> *)
-(*     let name = gd.qname (Symb.to_string tname |> String.uncapitalize) in *)
-(*     match tdef with *)
-(*       | EnumDef labels -> *)
-(*           let constrs = List.map (fun (l, _) -> translate_label gd l) labels in *)
-(*           gd.tdefs <- SMap.add tname name gd.tdefs; *)
-(*           Ptype { t_name = name; *)
-(*                   t_desc = Type_enum constrs; *)
-(*                   t_loc = Location.no_location } :: typs *)
-(*   end typdefs [] *)
+let decl_typs modul_name typdefs =
+  let qualify name = { qual = modul modul_name; name } in
+  fold_typdefs begin fun tname tdef (types, typ_symbs) ->
+    let name = qualify (Symb.to_string tname |> String.uncapitalize) in
+    match tdef with
+      | EnumDef labels, _ ->
+          let constrs = List.map (fun (l, _) ->
+            qualify (Symb.to_string (label_symb l))) labels in
+          (Ptype { t_name = name;
+                   t_desc = Type_enum constrs;
+                   t_loc = Location.no_location } :: types,
+           SMap.add tname name typ_symbs)
+  end typdefs ([], no_typ_symbs)
 
-let decl_typs_from_module_itf gd =
+let decl_typs_from_module_itf modul_name =
   (* Note we need to sort type declarations according to their respective
      dependencies; hence the implicit topological traversal of the type
      definitions. *)
-  let rec decl_types rem types =
+  let rec decl_types rem acc =
     if QualEnv.is_empty rem then
-      types
+      acc
     else
       let t_name, tdef = QualEnv.choose rem in
-      let rem, types = decl_typ t_name tdef rem types in
-      decl_types rem types
-  and decl_typ t_name tdef rem types =
+      let rem, acc = decl_typ t_name tdef rem acc in
+      decl_types rem acc
+  and decl_typ t_name tdef rem ((types, typ_symbs) as acc) =
     let rem = QualEnv.remove t_name rem in
-    if tdef = Tabstract || t_name.qual = Names.Pervasives then
-      rem, types
+    if t_name.qual <> modul_name then
+      rem, acc
     else
-      let t_desc, rem, types = match tdef with
+      let t_desc, rem, (types, typ_symbs) = match tdef with
         | Tenum cl ->
             (* Compiler_utils.info "declaring enum type %s" (shortname t_name); *)
             let name = Symb.of_string (String.capitalize (shortname t_name)) in
-            gd.tdefs <- SMap.add name t_name gd.tdefs;
-            (Type_enum cl, rem, types)
+            (Type_enum cl, rem, (types, SMap.add name t_name typ_symbs))
         | Talias (Tid tn) when tn.qual = t_name.qual ->    (* declare deps 1st *)
             (* Compiler_utils.info "declaring alias type %s" (shortname t_name); *)
             let tdef = QualEnv.find tn rem in
-            let rem, types = decl_typ tn tdef (QualEnv.remove tn rem) types in
-            (Type_alias (Tid tn), rem, types)
+            let rem, acc = decl_typ tn tdef (QualEnv.remove tn rem) acc in
+            (Type_alias (Tid tn), rem, acc)
         | Talias t ->
             (* Compiler_utils.info "declaring alias type %s" (shortname t_name); *)
-            (Type_alias t, rem, types)
+            (Type_alias t, rem, acc)
         | Tstruct _ ->
             failwith (asprintf "Unexpected struct type `%s' in module interface"
                         (shortname t_name))
         | Tabstract -> assert false
       in
-      rem, Ptype { t_name; t_desc; t_loc = Location.no_location; } :: types
+      rem, (Ptype { t_name; t_desc; t_loc = Location.no_location } :: types,
+            typ_symbs)
   in
-  decl_types Modules.g_env.Modules.types []
+  Modules.open_module modul_name;
+  decl_types Modules.g_env.Modules.types ([], no_typ_symbs)
 
 (* --- *)
 
@@ -391,19 +394,20 @@ let node_of_func gd ?node_sig n_name func =
 
 (* --- *)
 
-let gen_func ?node_sig ~node_name func =
+let gen_func ?typ_symbs ?node_sig ~node_name func =
   let { fn_typs; fn_decls } = func_desc func in
-  let modul = modul node_name in
-  let gd = mk_gen_data modul (fn_decls:> ('f, 'f var_spec) decls) fn_typs in
-  (* let typs = decl_typs fn_typs gd in *)
-  let typs = decl_typs_from_module_itf gd in
+  let fn_decls = (fn_decls :> ('f, 'f var_spec) decls) in
+  let typs, typ_symbs = match typ_symbs with
+    | None -> decl_typs node_name fn_typs
+    | Some typ_symbs -> [], typ_symbs
+  in
+  let gd = mk_gen_data node_name typ_symbs fn_decls fn_typs in
   let node = node_of_func gd ?node_sig node_name func in
-  node, typs
+  node :: typs
 
 (* --- *)
 
 let create_prog ?(open_modul = []) modul =
-  Modules.open_module modul;
   {
     p_modname = modul;
     p_opened = open_modul;
diff --git a/compiler/main/ctrl2ept.ml b/compiler/main/ctrl2ept.ml
index 3dd0c56..970198f 100644
--- a/compiler/main/ctrl2ept.ml
+++ b/compiler/main/ctrl2ept.ml
@@ -118,33 +118,18 @@ let parse_input ?filename (parse: ?filename:string -> _) =
 
 exception Error of string
 
-(* let hack_filter_inputs = let open AST in function *)
-(*   | `Desc ({ fn_decls = decls } as f) -> *)
-(*       (\* TODO: we should actually _substitute_ these variables with ff in the *)
-(*          definitions; yet I think they are unlikely to appear anywhere in the *)
-(*          controller. *\) *)
-(*       let init_symb = Symb.of_string Ctrln_utils.init_cond_str *)
-(*       and sink_symb = Symb.of_string Ctrln_utils.sink_state_str in *)
-(*       let decls = SMap.remove init_symb decls in *)
-(*       let decls = SMap.remove sink_symb decls in *)
-(*       `Desc { f with fn_decls = decls } *)
-(*   | _ -> failwith "should be given an unchecked function!" *)
-
-let parse_n_gen_ept_node ?filename ?node_name ?node_sig () =
+let parse_n_gen_ept_node ?filename ?node_name ?node_sig ?typ_symbs () =
   let name, func = parse_input ?filename CtrlNbac.Parser.Unsafe.parse_func in
   let node_name = match node_name with Some n -> n
     | None -> match name with None -> assert false
         | Some n -> Names.local_qn (n ^ "_ctrlr")
   in
-  (* let name = match name with None -> "ctrlr" | Some n -> n ^"_ctrlr" in *)
-  (* let func = hack_filter_inputs func in *)
-  name, CtrlNbacAsEpt.gen_func ~node_name ?node_sig func
+  name, CtrlNbacAsEpt.gen_func ?typ_symbs ~node_name ?node_sig func
 
 let handle_ctrlf ?filename mk_oc =
-  let _, (node, typs) = parse_n_gen_ept_node ?filename () in
+  let _, decls = parse_n_gen_ept_node ?filename () in
   let prog = CtrlNbacAsEpt.create_prog Names.LocalModule in    (* don't care? *)
-  let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
-  let prog = CtrlNbacAsEpt.add_to_prog node prog in
+  let prog = List.fold_right CtrlNbacAsEpt.add_to_prog decls prog in
   let oc, close = mk_oc.out_exec "ept" in
   Hept_printer.print oc prog;
   close ()
@@ -162,27 +147,24 @@ let output_prog prog modul =
   Hept_printer.print oc prog;
   close_out oc
 
-let input_function prog filename node_name node_sig =
+let input_function prog typ_symbs filename node_name node_sig =
   info "Reading function from `%s'…" filename;
-  let res = parse_n_gen_ept_node ~filename ~node_name ~node_sig () in
-  let node, typs = snd res in
-  (* XXX: check types are also in signature? maybe we should only use the types
+  let _, decls = parse_n_gen_ept_node ~filename ~node_name ~node_sig ~typ_symbs () in
+  (* XXX: check types are also in signature? actually, we only use the types
      declared in the signature instead, as long as the controller synthesis tool
      does not introduce new types. *)
-  let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
-  let prog = CtrlNbacAsEpt.add_to_prog node prog in
-  prog
+  List.fold_right CtrlNbacAsEpt.add_to_prog decls prog
 
-let try_ctrlf nn prog =
+let try_ctrlf typ_symbs nn prog =
   let node_name = Ctrln_utils.controller_node nn in
   if Modules.check_value node_name then
     let filename = Ctrln_utils.ctrlf_for_node nn in
     let node_sig = Modules.find_value node_name in
-    input_function prog filename node_name node_sig
+    input_function prog typ_symbs filename node_name node_sig
   else
     raise (Error "Unable to load any controller function.")
 
-let try_ctrls nn prog =
+let try_ctrls typ_symbs nn prog =
   let rec try_ctrls num prog =
     let node_name = Ctrln_utils.controller_node ~num nn in
     if Modules.check_value node_name then
@@ -190,7 +172,7 @@ let try_ctrls nn prog =
       if num = 0 && not (Sys.file_exists filename) then
         raise Exit;                                                  (* abort *)
       let node_sig = Modules.find_value node_name in
-      let prog = input_function prog filename node_name node_sig in
+      let prog = input_function prog typ_symbs filename node_name node_sig in
       try_ctrls (succ num) prog
     else
       prog
@@ -207,8 +189,12 @@ let handle_node arg =
   Modules.open_module Names.Pervasives;
   info "Loading module of controllers for node %s…" (Names.fullname nn);
   let om = Ctrln_utils.controller_modul mo in
+  info "Translating type declarations of module %s…" (Names.modul_to_string om);
+  let typs, typ_symbs = CtrlNbacAsEpt.decl_typs_from_module_itf om in
   let prog = CtrlNbacAsEpt.create_prog ~open_modul:[ ] om in
-  let prog = try try_ctrls nn prog with Exit -> try_ctrlf nn prog in
+  let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
+  let prog = try try_ctrls typ_symbs nn prog with
+    | Exit -> try_ctrlf typ_symbs nn prog in
   output_prog prog om
 
 (* -------------------------------------------------------------------------- *)