diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index dc44b223a8638602b609c3cdee2b318f28b07373..570067c07b196e5e0b7479f4891365a7a097d30a 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -21,22 +21,50 @@
 (**************************************************************************)
 
 module L = Wp_parameters
+module P = Why3.Pmodule
+module F = Filepath.Normalized
+module W = Why3
+module WConf = Why3.Whyconf
 
 (* -------------------------------------------------------------------------- *)
 
+let create_why3_env =
+    begin fun () ->
+      W.Env.create_env (WConf.loadpath (WConf.get_main (WConf.read_config None)))
+    end
+
 let () =
   Boot.Main.extend
     begin fun () ->
       let libs = L.Library.get () in
       List.iter
         (fun dir ->
-           L.debug ~level:0 " + LIB %a@." Filepath.Normalized.pretty dir
-        ) libs ;
+          L.debug ~level:0 " + LIBS %s@." dir
+        ) (F.to_string_list libs) ;
       let thys = L.Import.get () in
       List.iter
         (fun thy ->
            L.debug ~level:0 " + THY %s@." thy
         ) thys ;
+
+      let libs = L.Library.get () in
+      let thys = L.Import.get () in
+      let env = create_why3_env () in
+      List.iter
+      (fun thy ->
+         let ns = (P.read_module env (F.to_string_list libs) thy).mod_export in
+         let _t = List.map (fun (ity : W.Ity.itysymbol) -> ity.its_ts) (W.Wstdlib.Mstr.values (ns.ns_ts)) in
+         List.iter (
+          fun _ty ->
+            match W.Ty.ts_hash _ty with
+            | 1 -> L.debug "NoDef %s@." thy
+            | _ -> L.debug "Otr %s@." thy
+         ) _t;
+      ) thys ;
+      (* let _ns = (P.read_module env (F.to_string_list libs) (List.hd thys)).mod_export in
+      L.debug ""; *)
+
+
     end
 
 (* -------------------------------------------------------------------------- *)