diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli
new file mode 100644
index 0000000000000000000000000000000000000000..248efd321e0e0eb13b430fe4f8b6d971c3b27701
--- /dev/null
+++ b/src/session/session_itp.mli
@@ -0,0 +1,705 @@
+
+(** New Proof sessions ("Refectoire") *)
+
+type proof_attempt = {
+  prover
+  timelimit
+  memlimit
+  proof_state : Call_provers.prover_result option;  (* None means that the call was not done
+                                                       or never returned *)
+  proof_obsolete : bool;
+  proof_script : string option;  (* non empty for external ITP *)
+}
+
+
+(* note: la fonction register des transformations doit permettre de declarer les types des arguments
+
+  type trans_arg_type = TTint | TTstring | TTterm | TTty | TTtysymbol | TTlsymbol | TTprsymbol
+
+*)
+
+type trans_arg =
+  | TAint of int
+  | TAstring of string
+  | TAterm of Term.term
+  | TAty of ty
+  | TAtysymbol of tysymbol
+  | ...
+
+
+type transformation = {
+  transf_name : (task Task.string | task Task.tlist)   ou string
+  transf_args : trans_arg list
+  transf_subtasks : sequence of proof_task
+  }
+
+and proof_task =
+  {
+     why3_task : Task.task
+     externals_proofs : collection of proof_attempt
+     transf : sequence of transformation
+  }
+
+
+type goal =
+  { goal_task : proof_task
+    goal_origin : name of goal, its theory, its file
+  }
+
+
+type session =
+  {
+    goals : collection of goals
+
+    (* autre choix : collection de proof task, chaque task connait son parent
+
+       autrement dit l'arbre est a l'envers
+
+       avantage : recherche d'une task tres rapide, mise a jour des parents faciles
+
+       inconvenient : effacer un noeud demande de savoir effacer tous les descendants.
+
+     *)
+  }
+
+val add_proof_attempt : session -> path_to_a_proof_task (int list ?) -> proof_attempt -> session
+
+val add_transf : session -> path_to_a_proof_task (int list ?) -> transformation -> session
+
+
+
+
+(*
+
+  couche au-dessus: "scheduler" cad modifications asynchrones de la session
+
+   - gere une file de travaux de modifications a faire
+   - recupere les resultats de travaux , et les applique s'ils sont encore valides
+
+*)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+type theory =
+  {
+    goals : sequence of task
+  }
+
+type file =
+  {
+    theories = sequence of theories
+  }
+
+type session =
+  {
+    session_files : set of files
+  }
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+open Stdlib
+
+val debug : Debug.flag
+(** The debug flag "session" *)
+
+module PHstr : Exthtbl.Private with type key = string
+module PHprover : Exthtbl.Private with type key = Whyconf.prover
+
+(** {2 Proof attempts} *)
+
+(** State of a proof *)
+type proof_attempt_status =
+    | Unedited (** editor not yet run for interactive proof *)
+    | JustEdited (** edited but not run yet *)
+    | Interrupted (** external proof has never completed *)
+    | Scheduled (** external proof attempt is scheduled *)
+    | Running (** external proof attempt is in progress *)
+    | Done of Call_provers.prover_result (** external proof done *)
+    | InternalFailure of exn (** external proof aborted by internal error *)
+
+type expl
+(** An explanation gives hint about how the goal has been produced.
+    Allow to reattach proof_attempt to goal when the source file has been
+    modified.
+*)
+
+type task_option
+(** The task can be removed and later reconstructible *)
+
+type 'a hide
+(** For internal use *)
+
+
+type ident_path =
+  { ip_library : string list;
+    ip_theory : string;
+    ip_qualid : string list;
+  }
+
+type meta_args = Theory.meta_arg list
+module Mmeta_args : Extmap.S with type key = meta_args
+module Smeta_args : Extset.S with module M = Mmeta_args
+
+type metas_args = Smeta_args.t Mstr.t
+module Mmetas_args : Extmap.S with type key = metas_args
+
+type idpos = {
+  idpos_ts : ident_path Ty.Mts.t;
+  idpos_ls : ident_path Term.Mls.t;
+  idpos_pr : ident_path Decl.Mpr.t;
+}
+
+(** {2 Session} *)
+
+(** All the element of a session contain a key which can hold whatever
+    information the user want. It is generated by the keygen argument
+    of the functions of this module *)
+
+type 'a goal = private
+    { mutable goal_key  : 'a;
+      goal_name : Ident.ident; (** The ident of the task *)
+      goal_expl : expl;
+      goal_parent : 'a goal_parent;
+      mutable goal_checksum : Termcode.checksum option;  (** checksum of the task *)
+      mutable goal_shape : Termcode.shape;  (** shape of the task *)
+      mutable goal_verified : float option;
+      mutable goal_task: task_option;
+      mutable goal_expanded : bool;
+      goal_external_proofs : 'a proof_attempt PHprover.t;
+      goal_transformations : 'a transf PHstr.t;
+      mutable goal_metas : 'a metas Mmetas_args.t;
+    }
+
+and 'a proof_attempt = private
+    { proof_key : 'a;
+      mutable proof_prover : Whyconf.prover;
+      proof_parent : 'a goal;
+      mutable proof_state : proof_attempt_status;
+      mutable proof_timelimit : int;
+      mutable proof_memlimit : int;
+      mutable proof_obsolete : bool;
+      mutable proof_archived : bool;
+      mutable proof_edited_as : string option;
+    }
+
+and 'a goal_parent = private
+                     | Parent_theory of 'a theory
+                     | Parent_transf of 'a transf
+                     | Parent_metas  of 'a metas
+
+and 'a metas =
+  { mutable metas_key : 'a;
+    metas_added : metas_args;
+    metas_idpos : idpos;
+    metas_parent : 'a goal;
+    mutable metas_verified : float option;
+    mutable metas_goal : 'a goal;
+    (** Not mutated after the creation *)
+    mutable metas_expanded : bool;
+  }
+
+and 'a transf = private
+    { mutable transf_key : 'a;
+      transf_name : string;
+      (** Why3 transformation name *)
+      transf_parent : 'a goal;
+      mutable transf_verified : float option;
+      mutable transf_goals : 'a goal list;
+      (** Not mutated after the creation *)
+      mutable transf_expanded : bool;
+      mutable transf_detached : 'a detached option;
+    }
+
+and 'a detached = private
+    { detached_goals: 'a goal list; }
+
+and 'a theory = private
+    { mutable theory_key : 'a;
+      theory_name : Ident.ident;
+      theory_parent : 'a file;
+      mutable theory_checksum : Termcode.checksum option;
+      mutable theory_goals : 'a goal list;
+      (** Not mutated after the creation *)
+      mutable theory_verified : float option;
+      mutable theory_expanded : bool;
+      mutable theory_task : Theory.theory hide;
+      mutable theory_detached : 'a detached option;
+    }
+
+and 'a file = private
+    { mutable file_key : 'a;
+      file_name : string;
+      file_format : string option;
+      file_parent : 'a session;
+      mutable file_theories: 'a theory list;
+      (** Not mutated after the creation *)
+      mutable file_verified : float option;
+      mutable file_expanded : bool;
+      mutable file_for_recovery : Theory.theory Mstr.t hide;
+    }
+
+and 'a session = private
+    { session_files : 'a file PHstr.t;
+      mutable session_shape_version : int;
+      session_prover_ids : int PHprover.t;
+      session_dir   : string;
+    }
+
+val print_session : Format.formatter -> 'a session -> unit
+(** Print a session with a pstree format (cf Tree module) *)
+
+val print_attempt_status : Format.formatter -> proof_attempt_status -> unit
+
+val print_external_proof : Format.formatter -> 'key proof_attempt -> unit
+
+val create_session : ?shape_version:int -> string -> 'key session
+(** create a new session in the given directory. The directory is
+    created if it doesn't exists yet. Don't change the current
+    directory of the program if you give a relative path *)
+
+val get_project_dir : string -> string
+(** find the session which corresponds to the given file or return
+    directly the given directory;
+    return [Not_found] if the file or the directory doesn't exists
+*)
+
+(** {2 Read/Write} *)
+
+type 'key keygen = ?parent:'key -> unit -> 'key
+(** type of functions which can generate keys *)
+
+exception ShapesFileError of string
+exception SessionFileError of string
+
+val read_session: string -> unit session * bool
+(** Read a session stored on the disk. It returns a session without any
+    task attached to goals.
+
+    The returned boolean is set when there was shapes read from disk.
+
+    raises [SessionFileError msg] if the database file cannot be read
+    correctly.
+
+    raises [ShapesFileError msg] if the database extra file for shapes
+    cannot be read.
+
+*)
+
+val save_session : Whyconf.config -> 'key session -> unit
+(** Save a session on disk *)
+
+(** {2 Context of a session} *)
+
+(** A session which contains task and proof_attempt depends on an
+    environment and a prover configuration.
+    Loaded provers are cached in order to load drivers once *)
+
+type loaded_prover =
+    { prover_config : Whyconf.config_prover;
+      prover_driver : Driver.driver}
+
+type loaded_provers = loaded_prover option PHprover.t
+
+type 'a env_session = private
+    { env : Env.env;
+      mutable whyconf : Whyconf.config;
+      loaded_provers : loaded_provers;
+      mutable files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
+      session : 'a session}
+
+val update_env_session_config : 'a env_session -> Whyconf.config -> unit
+(** updates the configuration *)
+
+val load_prover : 'a env_session -> Whyconf.prover -> loaded_prover option
+(** load a prover *)
+
+val unload_provers : 'a env_session -> unit
+(** forces unloading of all provers,
+    to force reading again the configuration *)
+
+(** {2 Update session} *)
+
+exception OutdatedSession
+
+type 'key update_context =
+  { allow_obsolete_goals : bool;
+    release_tasks : bool;
+    use_shapes_for_pairing_sub_goals : bool;
+    keygen : 'key keygen;
+  }
+
+val update_session : ctxt:'key update_context -> 'oldkey session ->
+  Env.env -> Whyconf.config -> 'key env_session * bool * bool
+(** reload the given session with the given environnement :
+    - the files are reloaded
+    - apply again the transformation
+    - if some goals appear try to find to which goal
+    in the given session it corresponds.
+
+    The last case meant that the session was obsolete.
+    It is authorized if [allow_obsolete] is [true],
+    otherwise the exception {!OutdatedSession} is raised.
+    If the session was obsolete is indicated by
+    the second result.
+    If the merge generated new unpaired goals is indicated by
+    the third result.
+
+    raises [OutdatedSession] if the session is obsolete and
+    [allow_obsolete] is false
+
+*)
+
+(** {2 Copy/Paste } *)
+
+val copy_proof:  'a proof_attempt -> 'a proof_attempt
+val copy_transf: 'a transf        -> 'a transf
+val copy_metas:  'a metas         -> 'a metas
+(** keys are copied *)
+
+val add_proof_to_goal :
+  keygen:'a keygen -> 'a env_session ->
+  'a goal -> 'a proof_attempt ->'a proof_attempt
+val add_transf_to_goal:
+  keygen:'a keygen -> 'a env_session ->
+  'a goal -> 'a transf        -> 'a transf
+val add_metas_to_goal :
+  keygen:'a keygen -> 'a env_session ->
+  'a goal -> 'a metas         -> 'a metas
+(** keys are normally generated *)
+
+(** {2 Accessor} *)
+
+exception NoTask
+val goal_task : 'key goal -> Task.task
+(** Return the task of a goal. Raise {!NoTask} if the goal doesn't contain a task
+    (equivalent to ['key = notask] if {!release_task} is not used) *)
+
+val goal_task_option : 'key goal -> Task.task option
+(** Return the task of a goal. *)
+
+val goal_expl : 'key goal -> string
+(** Return the explication of a goal *)
+
+val proof_verified : 'key proof_attempt -> float option
+(** Return [Some t] if the proof is not obsolete and the result is
+    valid. [t] is the time needed to solved it *)
+
+val get_used_provers : 'a session -> Whyconf.Sprover.t
+(** Get the set of provers which appear in the session *)
+
+(* val metas_of_virtuals : 'a metas -> Theory.Smeta.t *)
+(* (\** Get the set of metas added (the parent goal must contain a task) *\) *)
+
+(** {2 Modificator} *)
+
+val set_transf_expanded : 'key transf -> bool -> unit
+val set_metas_expanded : 'key metas -> bool -> unit
+val set_goal_expanded : 'key goal -> bool -> unit
+val set_theory_expanded : 'key theory -> bool -> unit
+val set_file_expanded : 'key file -> bool -> unit
+(** open one level or close all the sub-level *)
+
+(** {2 General type} *)
+
+type 'a any =
+  | File of 'a file
+  | Theory of 'a theory
+  | Goal of 'a goal
+  | Proof_attempt of 'a proof_attempt
+  | Transf of 'a transf
+  | Metas of 'a metas
+
+val print_any : Format.formatter -> 'a any -> unit
+(** Print a subtree with a pstree format (cf Tree module) *)
+
+val key_any : 'a any -> 'a
+(** return the key of an element of the tree *)
+
+(** {2 External proof} *)
+
+type 'key notify = 'key any -> unit
+(** type of functions which notify modification of the verified field *)
+
+val add_external_proof :
+  ?notify:'key notify ->
+  keygen:'key keygen ->
+  obsolete:bool ->
+  archived:bool ->
+  timelimit:int ->
+  memlimit:int ->
+  edit:string option ->
+  'key goal ->
+  Whyconf.prover ->
+  proof_attempt_status ->
+  'key proof_attempt
+
+val remove_external_proof : ?notify:'key notify -> 'key proof_attempt -> unit
+
+val set_proof_state :
+  ?notify:'key notify ->
+  obsolete:bool ->
+  archived:bool ->
+  proof_attempt_status ->
+  'key proof_attempt -> unit
+
+val change_prover : 'a proof_attempt -> Whyconf.prover -> unit
+
+val set_obsolete : ?notify:'key notify -> 'key proof_attempt -> unit
+
+val set_archived : 'key proof_attempt -> bool -> unit
+
+val set_edited_as : string option -> 'key proof_attempt -> unit
+
+val get_edited_as_abs : 'key session -> 'k proof_attempt -> string option
+(** return the edited filename after concatenation to [session_dir] *)
+
+val update_edit_external_proof :
+  cntexample:bool -> 'key env_session -> 'key proof_attempt -> string
+(** return the absolute path of the edited file update with the
+    current goal *)
+
+
+val set_timelimit : int -> 'key proof_attempt -> unit
+val set_memlimit : int -> 'key proof_attempt -> unit
+
+val copy_external_proof :
+  ?notify:'key notify ->
+  keygen:'key keygen ->
+  ?obsolete:bool ->
+  ?archived:bool ->
+  ?timelimit:int ->
+  ?memlimit:int ->
+  ?edit:string option ->
+  ?goal:'key goal ->
+  ?prover:Whyconf.prover ->
+  ?attempt_status:proof_attempt_status ->
+  ?env_session:'key env_session ->
+  ?session:'key session ->
+  'key proof_attempt -> 'key proof_attempt
+(** copy an external proof.
+    if env_session and session are given only env_session.session is
+    taken into account.
+    The edited file is copied and an env_session is not required if :
+    {ul
+    {- the goal is not modified}
+    {- the prover is not modified}
+    {- a session is given}
+    }
+    The edited file is regenerated if
+    {ul
+    {- the external proof contain an edited file}
+    {- an env_session is given}
+    {- the given goal (or the old one if not modified) contain a task}
+    }
+    In all the other case the resulting external proof is considered
+    not edited.
+*)
+
+(** {2 Transformation} *)
+
+val add_transformation :
+  ?init:'key notify ->
+  ?notify:'key notify ->
+  keygen:'key keygen ->
+  'key env_session ->
+  string ->
+  'key goal ->
+  Task.task list ->
+  'key transf
+(** Add a transformation by its subgoals *)
+
+val add_registered_transformation :
+  keygen:'key keygen ->
+  'key env_session ->
+  string ->
+  'key goal ->
+  'key transf
+(** Apply a real transformation by its why3 name,
+    raise {!NoTask} if the goal doesn't contain a task.
+    If the goal already has a transformation with this name,
+    it is returned. *)
+
+val remove_transformation : ?notify:'key notify -> 'key transf -> unit
+  (** Remove a transformation *)
+
+(** {2 Metas} *)
+val add_registered_metas :
+  keygen:'key keygen ->
+  'key env_session ->
+  (string * Theory.meta_arg list) list ->
+  'key goal ->
+  'key metas
+(** Add some metas to a task. If the goal already contain a {!metas}
+    with same metas, the old one is returned.
+*)
+
+val remove_metas : ?notify:'key notify -> 'key metas -> unit
+(** Remove the addition of metas *)
+
+(** {2 File} *)
+
+val add_file :
+  keygen:'key keygen ->
+  'key env_session ->
+  ?format:string ->
+  string ->
+  'key file
+(** Add a real file by its filename. The filename must be relative to
+    session_dir *)
+
+val remove_file : 'key file -> unit
+(** Remove a file *)
+
+(** {2 Free and recover task} *)
+(** Tasks are stored inside the goals. For releasing memory you can remove
+    them. Later you can recompute them *)
+
+val release_task: 'a goal -> unit
+  (** remove the task stored in this goal*)
+
+val release_sub_tasks: 'a goal -> unit
+  (** apply the previous function on this goal and its its sub-goal *)
+
+val recover_theory_tasks: 'a env_session -> 'a theory -> unit
+  (** Recover all the sub-goal (not only strict) of this theory *)
+
+val goal_task_or_recover: 'a env_session -> 'a goal -> Task.task
+  (** same as goal_task but recover the task goal and all the one of this
+      theory if this goal task have been released *)
+
+(** {2 Iterators} *)
+
+(** {3 recursive} *)
+
+val goal_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key goal -> unit
+(* unused
+val transf_iter_proof_attempt :
+  ('key proof_attempt -> unit) -> 'key transf -> unit
+*)
+val theory_iter_proof_attempt :
+  ('key proof_attempt -> unit) -> 'key theory -> unit
+val transf_iter_proof_attempt :
+  ('key proof_attempt -> unit) -> 'key transf -> unit
+val file_iter_proof_attempt : ('key proof_attempt -> unit) -> 'key file -> unit
+val session_iter_proof_attempt :
+  ('key proof_attempt -> unit) -> 'key session -> unit
+val iter_proof_attempt :
+  ('key proof_attempt -> unit) -> 'key any -> unit
+
+val goal_iter_leaf_goal :
+  unproved_only:bool -> ('key goal -> unit) -> 'key goal -> unit
+(** iter all the goals which are a leaf
+    (no transformations are applied on it) *)
+
+val fold_all_sub_goals_of_theory :
+  ('a -> 'key goal -> 'a) -> 'a -> 'key theory -> 'a
+
+(** {3 not recursive} *)
+
+val iter_goal :
+  ('key proof_attempt -> unit) ->
+  ('key transf -> unit) ->
+  ('key metas -> unit) ->
+  'key goal -> unit
+val iter_transf :
+  ('key goal -> unit) -> 'key transf -> unit
+val iter_metas :
+  ('key goal -> unit) -> 'key metas -> unit
+val iter_theory : ('key goal -> unit) -> 'key theory -> unit
+  (** [iter_theory f th] applies [f] to all root goals of theory [th] *)
+val iter_file :
+  ('key theory -> unit) -> 'key file -> unit
+val iter_session :
+  ('key file -> unit) -> 'key session -> unit
+
+
+val goal_iter : ('key any -> unit) -> 'key goal -> unit
+(* unused
+val transf_iter : ('key any -> unit) -> 'key transf -> unit
+*)
+val theory_iter : ('key any -> unit) -> 'key theory -> unit
+val transf_iter : ('key any -> unit) -> 'key transf -> unit
+val metas_iter : ('key any -> unit) -> 'key metas -> unit
+val file_iter : ('key any -> unit) -> 'key file -> unit
+val session_iter : ('key any -> unit) -> 'key session -> unit
+val iter : ('key any -> unit) -> 'key any -> unit
+
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
+End:
+*)
+
+
+
+
+
+
+
+open Session
+
+val add_prover_call : ITP_state -> prover_name -> time limit -> ITP_state
+
+type 'args tactic = 'args -> (task list) trans
+
+val apply_tactic : ITP_state -> 'args tactic -> 'args -> ITP_state
+
+val remove_hyp : prsymbol tactic (* [remove_hyp H] remove the hypothesis H from the context *)
+
+val case_analysis : term tactic
+(* [case_analysis P] replaces task [H |- G] by two tasks [H, P |-G]  and [H, not P |- G] *)
+
+val assert_tactic : term tactic
+(* [assert_tactic P] replaces task [H |- G] by two tasks [H |- P] and [H,P |- G] *)
+
+val exists : term tactic
+(* [exists t] replaces task [H |- exists x. G ] by [ H |- G[x <- t]]  *)
+
+val instantiate : (pr_symbol,term) tactic
+(* [instantiate (H,t)] replaces task [....,H:forall x.P,... |- G ] by
+[ ....,H:forall x.P,...., P[x <- t] |- G ] *)
+
+val induction_on_nat : lsymbol ->
+
+
+
+(* display *)
+
+
+(* to display an ITP state: we need a driver for printing terms *)
+
+display : ITP_state -> driver -> list of strings (* ? *)