diff --git a/Makefile.in b/Makefile.in
index 2505045397e34c18edb0951473a4ced8195cf9c9..5aaac9aa183de5a701acb546cceeadd2578de81d 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1604,9 +1604,6 @@ endif
 
 ALTERGODIR=src/trywhy3/alt-ergo
 
-JSOCAMLCW=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.ppx \
-        -I src/ide
-
 JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
         -syntax camlp4o -I src/trywhy3 \
 	-I $(ALTERGODIR)/src/util \
@@ -1697,6 +1694,16 @@ clean::
 
 CLEANDIRS += src/trywhy3
 
+
+#########
+# why3webserver and full web/js interface
+#########
+
+ifeq (@HASJSOFOCAML,yes)
+
+JSOCAMLCW=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.ppx \
+        -I src/ide
+
 src/ide/why3_js.cmo: src/ide/why3_js.ml lib/why3/why3.cma
 	$(JSOCAMLCW) $(BFLAGS) -c $<
 
@@ -1709,6 +1716,7 @@ src/ide/why3_js.js: src/ide/why3_js.byte
 opt: lib/why3/why3.cma bin/why3webserver.opt src/ide/why3_js.js
 byte: lib/why3/why3.cma bin/why3webserver.byte src/ide/why3_js.js
 
+endif
 
 ########
 # bench
diff --git a/configure.in b/configure.in
index f49b834d949d6de890d6a076b9795121220d5c19..a41c4ed53af720fc52c34f16f06b22d6605042b5 100644
--- a/configure.in
+++ b/configure.in
@@ -484,6 +484,18 @@ dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)
 
 dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
 
+
+# js_of_ocaml
+
+JSOFOCAML=$(ocamlfind query js_of_ocaml)
+
+if test -z "$JSOFCAML"; then
+   HASJSOFOCAML=no
+   reason_jsofocaml=" (js_of_ocaml not found)"
+else
+   HASJSOFOCAML=yes
+fi
+
 # Coq
 
 enable_coq_support=yes
@@ -768,6 +780,8 @@ AC_SUBST(enable_ide)
 AC_SUBST(LABLGTK2LIB)
 AC_SUBST(LABLGTK2PKG)
 
+AC_SUBST(HASJSOFOCAML)
+
 AC_SUBST(META_OCAMLGRAPH)
 
 AC_SUBST(enable_zarith)
@@ -858,7 +872,8 @@ echo "    Library path            : $OCAMLLIB"
 echo "    Native compilation      : $enable_native_code"
 echo "    Profiling               : $enable_profiling"
 echo "Components"
-echo "    IDE command             : $enable_ide$reason_ide"
+echo "    GTK IDE                 : $enable_ide$reason_ide"
+echo "    Web IDE                 : $HASJSOFOCAML$reason_jsofocaml"
 echo "    GMP arithmetic          : $enable_zarith$reason_zarith"
 echo "    Compressed sessions     : $enable_zip$reason_zip"
 echo "    MenhirLib support       : $enable_menhirLib$reason_menhirLib"
diff --git a/examples/use_api/logic.ml b/examples/use_api/logic.ml
index 8e11799cbf38da75d0711af7c700337dd733f1c1..7ea6cf4b88682ebd9d11b1a12fe069d678f0ae3b 100644
--- a/examples/use_api/logic.ml
+++ b/examples/use_api/logic.ml
@@ -96,7 +96,7 @@ let result1 : Call_provers.prover_result =
   Call_provers.wait_on_call
     (Driver.prove_task ~limit:Call_provers.empty_limit
                        ~command:alt_ergo.Whyconf.command
-    alt_ergo_driver None task1)
+    alt_ergo_driver task1)
 
 (* prints Alt-Ergo answer *)
 let () = printf "@[On task 1, alt-ergo answers %a@."
@@ -106,7 +106,7 @@ let result2 : Call_provers.prover_result =
   Call_provers.wait_on_call
     (Driver.prove_task ~command:alt_ergo.Whyconf.command
     ~limit:{Call_provers.empty_limit with Call_provers.limit_time = 10}
-    alt_ergo_driver None task2)
+    alt_ergo_driver task2)
 
 let () = printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
   Call_provers.print_prover_answer result1.Call_provers.pr_answer
@@ -146,7 +146,7 @@ let result3 =
   Call_provers.wait_on_call
     (Driver.prove_task ~limit:Call_provers.empty_limit
                        ~command:alt_ergo.Whyconf.command
-    alt_ergo_driver None task3)
+    alt_ergo_driver task3)
 
 let () = printf "@[On task 3, alt-ergo answers %a@."
   Call_provers.print_prover_result result3
@@ -177,7 +177,7 @@ let result4 =
   Call_provers.wait_on_call
     (Driver.prove_task ~limit:Call_provers.empty_limit
                        ~command:alt_ergo.Whyconf.command
-    alt_ergo_driver None task4)
+    alt_ergo_driver task4)
 
 let () = printf "@[On task 4, alt-ergo answers %a@."
   Call_provers.print_prover_result result4
diff --git a/src/core/printer.ml b/src/core/printer.ml
index 95c83c5b6fe8d98b4701b3c8615f40d73fb73bfb..7685233a155f8b1df0e3e0924fc50dda80563492 100644
--- a/src/core/printer.ml
+++ b/src/core/printer.ml
@@ -35,7 +35,7 @@ type printer_mapping = {
 }
 
 type printer_args = {
-  name_table : name_tables option;
+  name_table : names_table option;
   env        : Env.env;
   prelude    : prelude;
   th_prelude : prelude_map;
diff --git a/src/core/printer.mli b/src/core/printer.mli
index f42d8511ebc45a925700166c74e7397215e2b9d9..c1919689db91691d7cfa7f0d6fc90b105abae399 100644
--- a/src/core/printer.mli
+++ b/src/core/printer.mli
@@ -36,7 +36,7 @@ type printer_mapping = {
 }
 
 type printer_args = {
-  name_table : name_tables option;
+  name_table : names_table option;
   env        : Env.env;
   prelude    : prelude;
   th_prelude : prelude_map;
diff --git a/src/core/task.ml b/src/core/task.ml
index 7841e622f2099f06c27c6fa833ece8b9914c8465..2e4da2e4f83f0f67e9f77e1ec205ef253826dfb7 100644
--- a/src/core/task.ml
+++ b/src/core/task.ml
@@ -345,7 +345,7 @@ let on_tagged_pr t task =
 (* Printing tasks *)
 type id_decl = (Decl.decl list) Ident.Mid.t
 
-type name_tables = {
+type names_table = {
     namespace : namespace;
     known_map : known_map;
     printer : ident_printer;
@@ -353,6 +353,13 @@ type name_tables = {
     id_decl : id_decl;
   }
 
+let empty_names_table = {
+    namespace = empty_ns;
+    known_map = Mid.empty;
+    printer = create_ident_printer [];
+    id_decl = Mid.empty;
+  }
+
 exception Bad_name_table of string
 
 (* Exception reporting *)
@@ -367,7 +374,7 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
   | NotExclusiveMeta m ->
       Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
   | Bad_name_table s ->
-      Format.fprintf fmt "Name table associated to task was not generated in %s" s
+      Format.fprintf fmt "Names table associated to task was not generated in %s" s
   | _ -> raise exn)
 
 (* task1 : prefix
diff --git a/src/core/task.mli b/src/core/task.mli
index 841987f784abf51cfeb000a689ee003c2176c91b..369e5af30171e783380bba01ed968444a5f4e408 100644
--- a/src/core/task.mli
+++ b/src/core/task.mli
@@ -129,14 +129,16 @@ val on_tagged_pr : meta -> task -> Spr.t
 (** Printing tasks *)
 type id_decl = (Decl.decl list) Ident.Mid.t
 
-type name_tables = {
+type names_table = {
     namespace : namespace;
     known_map : known_map;
     printer : ident_printer;
-(* Associate an id to a list of declarations in which it is used *)
+    (* Associate an id to a list of declarations in which it is used *)
     id_decl : id_decl;
   }
 
+val empty_names_table : names_table
+
 (** Exceptions *)
 
 exception Bad_name_table of string
diff --git a/src/core/trans.ml b/src/core/trans.ml
index 63a5b208f79d75fd99ec551a5ee46829f3ae6e2c..1c20e398802c9d7c34059954431de9e863e64447 100644
--- a/src/core/trans.ml
+++ b/src/core/trans.ml
@@ -335,8 +335,8 @@ let list_transforms_l () =
 
 (** transformations with arguments *)
 
-type trans_with_args = string list -> Env.env -> Task.name_tables -> task trans
-type trans_with_args_l = string list -> Env.env -> Task.name_tables -> task tlist
+type trans_with_args = string list -> Env.env -> Task.names_table -> task trans
+type trans_with_args_l = string list -> Env.env -> Task.names_table -> task tlist
 
 let transforms_with_args = Hstr.create 17
 let transforms_with_args_l = Hstr.create 17
diff --git a/src/core/trans.mli b/src/core/trans.mli
index 0200899e48fe7c7e3ff24f3f335430bb865b211a..a550151de0b43680389edae5b07758d7b8641697 100644
--- a/src/core/trans.mli
+++ b/src/core/trans.mli
@@ -164,8 +164,8 @@ val named : string -> 'a trans -> 'a trans
 
 *)
 
-type trans_with_args = string list -> Env.env -> Task.name_tables -> task trans
-type trans_with_args_l = string list -> Env.env -> Task.name_tables -> task tlist
+type trans_with_args = string list -> Env.env -> Task.names_table -> task trans
+type trans_with_args_l = string list -> Env.env -> Task.names_table -> task tlist
 
 val list_transforms_with_args   : unit -> (string * Pp.formatted) list
 val list_transforms_with_args_l : unit -> (string * Pp.formatted) list
@@ -188,5 +188,5 @@ val list_trans : unit -> string list
 val apply_transform : string -> Env.env -> task -> task list
 (** apply a registered 1-to-1 or a 1-to-n, directly.*)
 
-val apply_transform_args : string -> Env.env -> string list -> Task.name_tables -> task -> task list
+val apply_transform_args : string -> Env.env -> string list -> Task.names_table -> task -> task list
 (** apply a registered 1-to-1 or a 1-to-n or a trans with args, directly *)
diff --git a/src/driver/driver.mli b/src/driver/driver.mli
index 7ffa54e219e7987747fc85c1ab70b8609ed470da..6529edffa11d307622ea55d773983a298db49f80 100644
--- a/src/driver/driver.mli
+++ b/src/driver/driver.mli
@@ -46,12 +46,12 @@ val call_on_buffer :
 val print_task :
   ?old       : in_channel ->
   ?cntexample : bool ->
-  ?name_table: Task.name_tables ->
+  ?name_table: Task.names_table ->
   driver -> Format.formatter -> Task.task -> unit
 
 val print_theory :
   ?old       : in_channel ->
-  ?name_table: Task.name_tables ->
+  ?name_table: Task.names_table ->
   driver -> Format.formatter -> Theory.theory -> unit
   (** produce a realization of the given theory using the given driver *)
 
@@ -61,7 +61,7 @@ val prove_task :
   ?cntexample  : bool ->
   ?old         : string ->
   ?inplace     : bool ->
-  ?name_table  : Task.name_tables ->
+  ?name_table  : Task.names_table ->
   driver -> Task.task -> Call_provers.prover_call
 
 (** Split the previous function in two simpler functions *)
@@ -69,7 +69,7 @@ val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
 
 val print_task_prepared :
   ?old       : in_channel ->
-  ?name_table: Task.name_tables ->
+  ?name_table: Task.names_table ->
   driver -> Format.formatter -> Task.task -> Printer.printer_mapping
 
 val prove_task_prepared :
@@ -77,7 +77,7 @@ val prove_task_prepared :
   limit        : Call_provers.resource_limit ->
   ?old         : string ->
   ?inplace     : bool ->
-  ?name_table  : Task.name_tables ->
+  ?name_table  : Task.names_table ->
   driver -> Task.task -> Call_provers.prover_call
 
 
diff --git a/src/printer/why3printer.ml b/src/printer/why3printer.ml
index 2f47125509cffef7f04df1bd99f07b0e0e421b30..e5a6a7880b8eaf6945ce74d3b07f73a967c2e082 100644
--- a/src/printer/why3printer.ml
+++ b/src/printer/why3printer.ml
@@ -435,8 +435,8 @@ let print_task args ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
   (* forget_all (); *)
   let tables = match args.name_table with
-  | None -> raise (Bad_name_table "why3printer")
-  | Some tables -> tables in
+    | None -> empty_names_table (* raise (Bad_name_table "Why3printer.print_task")*)
+    | Some tables -> tables in
   print_prelude fmt args.prelude;
   fprintf fmt "theory Task@\n";
   print_th_prelude task fmt args.th_prelude;
@@ -462,8 +462,8 @@ let print_sequent args ?old:_ fmt task =
   info := {info_syn = Discriminate.get_syntax_map task;
     itp = true};
   let tables = match args.name_table with
-  | None -> raise (Bad_name_table "why3printer")
-  | Some tables -> tables in
+    | None -> empty_names_table (* raise (Bad_name_table "Why3printer.print_sequent") *)
+    | Some tables -> tables in
   (* let tables = build_name_tables task in *)
   let ut = Task.used_symbols (Task.used_theories task) in
   let ld = Task.local_decls task ut in
diff --git a/src/printer/why3printer.mli b/src/printer/why3printer.mli
index 1666c233487f119dc894bda3cfc380c9869156eb..b86bdc84773f35b481a19356a6ba592c2987b42e 100644
--- a/src/printer/why3printer.mli
+++ b/src/printer/why3printer.mli
@@ -30,12 +30,12 @@
 
 *)
 
-val print_ls   : Task.name_tables -> Format.formatter -> Term.lsymbol  -> unit
-val print_tv   : Task.name_tables -> Format.formatter -> Ty.tvsymbol   -> unit
-val print_ts   : Task.name_tables -> Format.formatter -> Ty.tysymbol   -> unit
-val print_forget_vsty : Task.name_tables -> Format.formatter -> Term.vsymbol  -> unit
-val print_pr   : Task.name_tables -> Format.formatter -> Decl.prsymbol -> unit
-val print_pat  : Task.name_tables -> Format.formatter -> Term.pattern  -> unit
-val print_ty   : Task.name_tables -> Format.formatter -> Ty.ty         -> unit
-val print_term : Task.name_tables -> Format.formatter -> Term.term     -> unit
-val print_decl : Task.name_tables -> Format.formatter -> Decl.decl     -> unit
+val print_ls   : Task.names_table -> Format.formatter -> Term.lsymbol  -> unit
+val print_tv   : Task.names_table -> Format.formatter -> Ty.tvsymbol   -> unit
+val print_ts   : Task.names_table -> Format.formatter -> Ty.tysymbol   -> unit
+val print_forget_vsty : Task.names_table -> Format.formatter -> Term.vsymbol  -> unit
+val print_pr   : Task.names_table -> Format.formatter -> Decl.prsymbol -> unit
+val print_pat  : Task.names_table -> Format.formatter -> Term.pattern  -> unit
+val print_ty   : Task.names_table -> Format.formatter -> Ty.ty         -> unit
+val print_term : Task.names_table -> Format.formatter -> Term.term     -> unit
+val print_decl : Task.names_table -> Format.formatter -> Decl.decl     -> unit
diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index d718c6cb61551251dd640c8d720f6df8f03fd303..ede8d08c2b4e0d69b624828f945d79df983dbc8c 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -467,10 +467,10 @@ let build_prover_call c id pr limit callback =
       config_pr
       ~with_steps:Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
   let task = Session_itp.get_task c.controller_session id in
-  let tables = Session_itp.get_tables c.controller_session id in
+  let table = Session_itp.get_table c.controller_session id in
   let call =
     Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
-                      ~limit ?name_table:tables driver task
+                      ~limit ?name_table:table driver task
   in
   let pa = (c.controller_session,id,pr,callback,false,call) in
   Queue.push pa prover_tasks_in_progress
@@ -571,13 +571,13 @@ let schedule_proof_attempt c id pr ~limit ~callback ~notification =
 let schedule_transformation_r c id name args ~callback =
   let apply_trans () =
     let task = get_task c.controller_session id in
-    let tables = match get_tables c.controller_session id with
-    | None -> raise (Task.Bad_name_table "schedule_transformation")
-    | Some tables -> tables in
+    let table = match get_table c.controller_session id with
+    | None -> raise (Task.Bad_name_table "Controller_itp.schedule_transformation_r")
+    | Some table -> table in
     begin
       try
         let subtasks =
-          Trans.apply_transform_args name c.controller_env args tables task in
+          Trans.apply_transform_args name c.controller_env args table task in
         (* if result is same as input task, consider it as a failure *)
         begin
           match subtasks with
diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 2a6f1e26e58829c4d90b25fade49be56e9784f73..27e14131f77b74c94d48d45470a13778b76da561 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -68,49 +68,49 @@ let loaded_strategies = ref []
 (****** Exception handling *********)
 
 let print_term s id fmt t =
-  let tables = match (Session_itp.get_tables s id) with
+  let tables = match (Session_itp.get_table s id) with
   | None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
   | Some tables -> tables in
   Why3printer.print_term tables fmt t
 
 let print_type s id fmt t =
-  let tables = match (Session_itp.get_tables s id) with
+  let tables = match (Session_itp.get_table s id) with
   | None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
   | Some tables -> tables in
   Why3printer.print_ty tables fmt t
 
 let print_ts s id fmt t =
-  let tables = match (Session_itp.get_tables s id) with
+  let tables = match (Session_itp.get_table s id) with
   | None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
   | Some tables -> tables in
   Why3printer.print_ts tables fmt t
 
 let print_ls s id fmt t =
-  let tables = match (Session_itp.get_tables s id) with
+  let tables = match (Session_itp.get_table s id) with
   | None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
   | Some tables -> tables in
   Why3printer.print_ls tables fmt t
 
 let print_tv s id fmt t =
-  let tables = match (Session_itp.get_tables s id) with
+  let tables = match (Session_itp.get_table s id) with
   | None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
   | Some tables -> tables in
   Why3printer.print_tv tables fmt t
 
 let print_vsty s id fmt t =
-  let tables = match (Session_itp.get_tables s id) with
+  let tables = match (Session_itp.get_table s id) with
   | None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
   | Some tables -> tables in
   Why3printer.print_forget_vsty tables fmt t
 
 let print_pr s id fmt t =
-  let tables = match (Session_itp.get_tables s id) with
+  let tables = match (Session_itp.get_table s id) with
   | None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
   | Some tables -> tables in
   Why3printer.print_pr tables fmt t
 
 let print_pat s id fmt t =
-  let tables = match (Session_itp.get_tables s id) with
+  let tables = match (Session_itp.get_table s id) with
   | None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
   | Some tables -> tables in
   Why3printer.print_pat tables fmt t
@@ -798,7 +798,7 @@ let get_locations t =
   (* -- send the task -- *)
   let task_of_id d id =
     let task = get_task d.cont.controller_session id in
-    let tables = get_tables d.cont.controller_session id in
+    let tables = get_table d.cont.controller_session id in
     (* This function also send source locations associated to the task *)
     let loc_color_list = get_locations task in
     Pp.string_of
diff --git a/src/session/server_utils.ml b/src/session/server_utils.ml
index d7d7004c0c28a113dae76c7884851f6f155d407b..ec8bd48e94dd540be18d6bf823e449eb38048002 100644
--- a/src/session/server_utils.ml
+++ b/src/session/server_utils.ml
@@ -137,7 +137,7 @@ let search_id _cont task args =
 
 type query =
   | Qnotask of (Controller_itp.controller -> string list -> string)
-  | Qtask of (Controller_itp.controller -> Task.name_tables -> string list -> string)
+  | Qtask of (Controller_itp.controller -> Task.names_table -> string list -> string)
 
 let help_on_queries fmt commands =
   let l = Stdlib.Hstr.fold (fun c (h,_) acc -> (c,h)::acc) commands [] in
@@ -294,10 +294,10 @@ let interp commands_table config cont id s =
     | Qnotask f, _ -> Query (f cont args)
     | Qtask _, None -> QError "please select a goal first"
     | Qtask f, Some id ->
-       let tables = match Session_itp.get_tables cont.Controller_itp.controller_session id with
-       | None -> raise (Task.Bad_name_table "interp")
-       | Some tables -> tables in
-       let s = try Query (f cont tables args) with
+       let table = match Session_itp.get_table cont.Controller_itp.controller_session id with
+       | None -> raise (Task.Bad_name_table "Server_utils.interp")
+       | Some table -> table in
+       let s = try Query (f cont table args) with
        | Undefined_id s -> QError ("No existing id corresponding to " ^ s)
        | Number_of_arguments -> QError "Bad number of arguments"
        in s
diff --git a/src/session/server_utils.mli b/src/session/server_utils.mli
index 422058620030a3f7cd8acb6950d360239f64fb93..5d602dcbb0cf5847c22c681494c00938fc95796c 100644
--- a/src/session/server_utils.mli
+++ b/src/session/server_utils.mli
@@ -17,11 +17,11 @@ exception Number_of_arguments
 
 type query =
   | Qnotask of (Controller_itp.controller -> string list -> string)
-  | Qtask of (Controller_itp.controller -> Task.name_tables -> string list -> string)
+  | Qtask of (Controller_itp.controller -> Task.names_table -> string list -> string)
 
 
-val print_id: 'a -> Task.name_tables -> string list -> string
-val search_id: 'a -> Task.name_tables -> string list -> string
+val print_id: 'a -> Task.names_table -> string list -> string
+val search_id: 'a -> Task.names_table -> string list -> string
 
 val list_provers: Controller_itp.controller -> _ -> string
 val list_transforms: unit -> (string * Pp.formatted) list
diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml
index 0858cb4bb18e5aceb4044e053965581a3a06679e..8514712989e9b99670504a2034a03d86c372b717 100644
--- a/src/session/session_itp.ml
+++ b/src/session/session_itp.ml
@@ -42,7 +42,7 @@ type proof_attempt_node = {
 type proof_node = {
   proofn_name                    : Ident.ident;
   proofn_task                    : Task.task;
-  proofn_table                   : Task.name_tables option;
+  proofn_table                   : Task.names_table option;
   proofn_parent                  : proof_parent;
   proofn_checksum                : Termcode.checksum option;
   proofn_shape                   : Termcode.shape;
@@ -207,7 +207,7 @@ let get_task (s:session) (id:proofNodeID) =
   let node = get_proofNode s id in
   node.proofn_task
 
-let get_tables (s: session) (id: proofNodeID) =
+let get_table (s: session) (id: proofNodeID) =
   let node = get_proofNode s id in
   node.proofn_table
 
@@ -1157,7 +1157,7 @@ let add_registered_transformation s env old_tr goal_id =
     Debug.dprintf debug "[merge_theory] trans not found@.";
     let task = goal.proofn_task in
     let tables = match goal.proofn_table with
-    | None -> raise (Task.Bad_name_table "add_registered_transformation")
+    | None -> raise (Task.Bad_name_table "Session_itp.add_registered_transformation")
     | Some tables -> tables in
     let subgoals = Trans.apply_transform_args old_tr.transf_name env old_tr.transf_args tables task in
     graft_transf s goal_id old_tr.transf_name old_tr.transf_args subgoals
diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli
index 3495e7fa454f495dbef4889dba8c0e47e2aec3f7..5e6c18bb31a3d5ea2047367048871e80b1acf930 100644
--- a/src/session/session_itp.mli
+++ b/src/session/session_itp.mli
@@ -73,7 +73,7 @@ val is_below: session -> any -> any -> bool
 type proof_parent = Trans of transID | Theory of theory
 
 val get_task : session -> proofNodeID -> Task.task
-val get_tables: session -> proofNodeID -> Task.name_tables option
+val get_table : session -> proofNodeID -> Task.names_table option
 
 val get_transformations : session -> proofNodeID -> transID list
 val get_proof_attempt_ids :
diff --git a/src/transform/args_wrapper.ml b/src/transform/args_wrapper.ml
index f4c866b73f488464edf0b5474aab3fdb643f3b56..81bb892c1e805991686aa6e87647389097413c47 100644
--- a/src/transform/args_wrapper.ml
+++ b/src/transform/args_wrapper.ml
@@ -50,7 +50,7 @@ type symb =
   | Pr of prsymbol
 
 (* [add_unsafe s id tables] Add (s, id) to tables without any checking. *)
-let add_unsafe (s: string) (id: symb) (tables: name_tables) : name_tables =
+let add_unsafe (s: string) (id: symb) (tables: names_table) : names_table =
   match id with
   | Ts ty ->
       {tables with
@@ -66,7 +66,7 @@ let add_unsafe (s: string) (id: symb) (tables: name_tables) : name_tables =
 }
 
 (* Adds symbols that are introduced to a constructor *)
-let constructor_add (cl: constructor list) tables : name_tables =
+let constructor_add (cl: constructor list) tables : names_table =
   List.fold_left
     (fun tables ((ls, cl): constructor) ->
       let tables = List.fold_left
@@ -139,7 +139,7 @@ let rec add_id tables d t =
 
 (* [add d printer tables] Adds all new declaration of symbol inside d to tables.
   It uses printer to give them a unique name and also register these new names in printer *)
-let add (d: decl) (tables: name_tables): name_tables =
+let add (d: decl) (tables: names_table): names_table =
   match d.d_node with
   | Dtype ty ->
       (* only current symbol is new in the declaration (see create_ty_decl) *)
@@ -188,7 +188,7 @@ let add (d: decl) (tables: name_tables): name_tables =
       let tables = add_unsafe s (Pr pr) tables in
       add_id tables d t
 
-let build_name_tables task : name_tables =
+let build_name_tables task : names_table =
   let pr = fresh_printer () in
   let km = Task.task_known task in
   let empty_decls = Ident.Mid.empty in
@@ -339,7 +339,7 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
     | Topt (s,t)     -> "opt [" ^ s ^ "] " ^ print_type t
     | Toptbool (s,t) -> "opt [" ^ s ^ "] -> " ^ print_type t
 
-let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> name_tables -> task -> b =
+let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> names_table -> task -> b =
   fun t f l env tables task ->
     match t, l with
     | Ttrans, _-> apply f task
@@ -410,7 +410,7 @@ let wrap_l : type a. (a, task list) trans_typ -> a -> trans_with_args_l =
 let wrap   : type a. (a, task) trans_typ -> a -> trans_with_args =
   fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
 
-let wrap_any : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> Task.name_tables -> b trans =
+let wrap_any : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> Task.names_table -> b trans =
   fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
 
 let wrap_and_register : type a b. desc:Pp.formatted -> string -> (a, b) trans_typ -> a -> unit =
diff --git a/src/transform/args_wrapper.mli b/src/transform/args_wrapper.mli
index 166deddabb5930d83ee4401b2a309a5b208f98e6..f863ebc1d60d1e8c5f97b7a56facd7987e26b4a2 100644
--- a/src/transform/args_wrapper.mli
+++ b/src/transform/args_wrapper.mli
@@ -11,7 +11,7 @@ exception Arg_hyp_not_found of string
 (** Pre-processing of tasks, to build unique names for all declared
     identifiers of a task.*)
 
-val build_name_tables : Task.task -> Task.name_tables
+val build_name_tables : Task.task -> Task.names_table
 
 type (_, _) trans_typ =
   | Ttrans    : (task Trans.trans, task) trans_typ