diff --git a/examples/stdlib/array/why3session.xml b/examples/stdlib/array/why3session.xml
index 842b827f918b48a31be96a7024b7dd6103bad912..ea77f929a6b5bac2ccd5e881fec42fafe913a83d 100644
--- a/examples/stdlib/array/why3session.xml
+++ b/examples/stdlib/array/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
-<why3session shape_version="4">
+<why3session shape_version="5">
 <prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Coq" version="8.7.1" timelimit="6" steplimit="0" memlimit="1000"/>
diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml
index c2eb78850e98da0130ffc29d38a3d8712b564bc4..c522ab49e74d876adaef806ad24a51e718581a89 100644
--- a/src/session/controller_itp.ml
+++ b/src/session/controller_itp.ml
@@ -223,18 +223,18 @@ let print_session fmt c =
     find a corresponding new theory resp. old goal are kept, with
     tasks associated to them *)
 
-let reload_files (c : controller) ~use_shapes =
+let reload_files (c : controller) ~shape_version =
   let old_ses = c.controller_session in
   c.controller_env <- Env.create_env (Env.get_loadpath c.controller_env);
   Whyconf.Hprover.reset c.controller_provers;
   load_drivers c;
   c.controller_session <- empty_session ~from:old_ses (get_dir old_ses);
-  merge_files ~use_shapes c.controller_env c.controller_session old_ses
+  merge_files ~shape_version c.controller_env c.controller_session old_ses
 
 exception Errors_list of exn list
 
-let reload_files (c: controller) ~use_shapes =
-  let errors, b1, b2 = reload_files c ~use_shapes in
+let reload_files (c: controller) ~shape_version =
+  let errors, b1, b2 = reload_files c ~shape_version in
   match errors with
   | [] -> b1, b2
   | _ -> raise (Errors_list errors)
diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli
index 3cebd548685dd71b88bfa3d82897a6cec011da49..85bd76b4a91a2ccc08f6880e45ad984f3ce28d31 100644
--- a/src/session/controller_itp.mli
+++ b/src/session/controller_itp.mli
@@ -110,8 +110,17 @@ val print_session : Format.formatter -> controller -> unit
 
 exception Errors_list of exn list
 
-val reload_files : controller -> use_shapes:bool -> bool * bool
-(** reload the files of the given session:
+val reload_files : controller -> shape_version:int option -> bool * bool
+(** [reload_files] returns a pair [(o,d)]: [o] true means there are
+    obsolete goals, [d] means there are missed objects (goals,
+    transformations, theories or files) that are now detached in the
+    session returned.
+
+  If parsing or typing errors occurs, a list of errors is raised
+  inside exception Errors_list.
+
+  The detailed process of reloading the files of the given session is
+  as follows.
 
   - each file is parsed again and theories/goals extracted from it. If
     some syntax error or parsing error occurs, then the corresponding
@@ -155,13 +164,7 @@ val reload_files : controller -> use_shapes:bool -> bool * bool
       it, neither to its subgoals.
 
 
-  [reload_files] It returns a pair (o, d): o true means there are
-    obsolete goals, d means there are missed objects (goals, transformations,
-    theories or files) that are now detached in the session returned.
-   If parsing or typing errors occurs, a list of errors is raised inside
-   exception Errors_list.
-
-*)
+ *)
 
 val add_file : controller -> ?format:Env.fformat -> string -> unit
 (** [add_fil cont ?fmt fname] parses the source file
diff --git a/src/session/itp_server.ml b/src/session/itp_server.ml
index 51a859245f5bbe5b8eea5d5e87d1293e2e56304d..8406dc29b574b5ffbf2ce5148a719128a028cde2 100644
--- a/src/session/itp_server.ml
+++ b/src/session/itp_server.ml
@@ -595,10 +595,10 @@ end
 
   (* Reload_files that is used even if the controller is not correct. It can
      be incorrect and end up in a correct state. *)
-  let reload_files cont ~use_shapes =
+  let reload_files cont ~shape_version =
     capture_parse_or_type_errors
       (fun c ->
-        try let (_,_) = reload_files ~use_shapes c in [] with
+        try let (_,_) = reload_files ~shape_version c in [] with
         | Errors_list le -> le) cont
 
   let add_file cont ?format fname =
@@ -971,7 +971,7 @@ end
 
   let init_server ?(send_source=true) config env f =
     Debug.dprintf debug "loading session %s@." f;
-    let ses,use_shapes = Session_itp.load_session f in
+    let ses,shape_version = Session_itp.load_session f in
     Debug.dprintf debug "creating controller@.";
     let c = create_controller config env ses in
     let shortcuts =
@@ -1011,7 +1011,7 @@ end
                      };
     Debug.dprintf debug "reloading source files@.";
     let d = get_server_data () in
-    let x = reload_files d.cont ~use_shapes in
+    let x = reload_files d.cont ~shape_version in
     reset_and_send_the_whole_tree ();
     (* After initial sending, we don't check anymore that there is a need to
            focus on a specific node. *)
@@ -1273,7 +1273,9 @@ end
     let _old_focus = !focused_node in
     unfocus ();
     clear_tables ();
-    let l = reload_files d.cont ~use_shapes:true in
+    let l = reload_files d.cont
+                         ~shape_version:(Some Termcode.current_shape_version)
+    in
     reset_and_send_the_whole_tree ();
     match l with
     | [] ->
diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml
index 40653805b81131f382adc0cad14b8c495bff9db3..249c13ae06ab2e1a09309f86d9e1671374e6a6ff 100644
--- a/src/session/session_itp.ml
+++ b/src/session/session_itp.ml
@@ -65,8 +65,6 @@ type proof_node = {
   proofn_name                    : Ident.ident;
   proofn_expl                    : string;
   proofn_parent                  : proof_parent;
-  proofn_checksum                : Termcode.checksum;
-  proofn_shape                   : Termcode.shape;
   proofn_attempts                : proofAttemptID Hprover.t;
   mutable proofn_transformations : transID list;
 }
@@ -118,7 +116,7 @@ type session = {
   mutable next_transID          : int;
   session_dir                   : string; (** Absolute path *)
   session_files                 : file Hstr.t;
-  mutable session_shape_version : int;
+  session_sum_shape_table       : (Termcode.checksum * Termcode.shape) Hpn.t;
   session_prover_ids            : int Hprover.t;
   (* tasks *)
   session_raw_tasks : Task.task Hpn.t;
@@ -470,6 +468,7 @@ let print_proof_attempt fmt pa =
 
 let rec print_proof_node s (fmt: Format.formatter) p =
   let pn = get_proofNode s p in
+  let sum,_ = Hpn.find s.session_sum_shape_table p in
   let parent = match pn.proofn_parent with
   | Theory t -> t.theory_name.id_string
   | Trans id -> (get_transfNode s id).transf_name
@@ -477,7 +476,7 @@ let rec print_proof_node s (fmt: Format.formatter) p =
   fprintf fmt
     "@[<hv 1> Goal %s;@ parent %s;@ sum %s;@ @[<hv 1>[%a]@]@ @[<hv 1>[%a]@]@]"
     pn.proofn_name.id_string parent
-    (Termcode.string_of_checksum pn.proofn_checksum)
+    (Termcode.string_of_checksum sum)
     (Pp.print_list Pp.semi print_proof_attempt)
       (Hprover.fold (fun _key e l ->
                      let e = get_proof_attempt_node s e in
@@ -512,10 +511,10 @@ let _print_session fmt s =
 
 
 let empty_session ?from dir =
-  let prover_ids, shape_version =
+  let prover_ids =
     match from with
-    | Some v -> v.session_prover_ids, v.session_shape_version
-    | None -> Hprover.create 7, Termcode.current_shape_version
+    | Some v -> v.session_prover_ids
+    | None -> Hprover.create 7
   in
   { proofAttempt_table = Hint.create 97;
     next_proofAttemptID = 0;
@@ -525,10 +524,10 @@ let empty_session ?from dir =
     next_transID = 0;
     session_dir = dir;
     session_files = Hstr.create 3;
-    session_shape_version = shape_version;
     session_prover_ids = prover_ids;
     session_raw_tasks = Hpn.create 97;
     session_task_tables = Hpn.create 97;
+    session_sum_shape_table = Hpn.create 97;
     file_state = Hstr.create 3;
     th_state = Ident.Hid.create 7;
     tn_state = Htn.create 97;
@@ -576,41 +575,39 @@ let graft_proof_attempt ?file (s : session) (id : proofNodeID) (pr : Whyconf.pro
 
 (* [mk_proof_node s n t p id] register in the session [s] a proof node
    of proofNodeID [id] of parent [p] of task [t] *)
-let mk_proof_node ~version ~expl (s : session) (n : Ident.ident) (t : Task.task)
+let mk_proof_node ~shape_version ~expl (s : session) (n : Ident.ident) (t : Task.task)
     (parent : proof_parent) (node_id : proofNodeID) =
-  (* let tables = Args_wrapper.build_naming_tables t in *)
-  let sum = Termcode.task_checksum ~version t in
-  let shape = Termcode.t_shape_task ~version ~expl t in
   let pn = { proofn_name = n;
              proofn_expl = expl;
              proofn_parent = parent;
-             proofn_checksum = sum;
-             proofn_shape = shape;
              proofn_attempts = Hprover.create 7;
              proofn_transformations = [] } in
+  Hint.add s.proofNode_table node_id pn;
   Hpn.add s.session_raw_tasks node_id t;
-  Hint.add s.proofNode_table node_id pn
+  let sum = Termcode.task_checksum ~version:shape_version t in
+  let shape = Termcode.t_shape_task ~version:shape_version ~expl t in
+  Hpn.add s.session_sum_shape_table node_id (sum,shape)
+
+let mk_new_proof_node = mk_proof_node ~shape_version:Termcode.current_shape_version
 
 let mk_proof_node_no_task (s : session) (n : Ident.ident)
     (parent : proof_parent) (node_id : proofNodeID) sum shape proved =
   let pn = { proofn_name = n;
              proofn_expl = "";
              proofn_parent = parent;
-             proofn_checksum = sum;
-             proofn_shape = shape;
              proofn_attempts = Hprover.create 7;
              proofn_transformations = [] } in
   Hint.add s.proofNode_table node_id pn;
+  Hpn.add s.session_sum_shape_table node_id (sum,shape);
   Hint.add s.pn_state node_id proved
 
-let mk_transf_proof_node (s : session) (parent_name : string)
+let mk_new_transf_proof_node (s : session) (parent_name : string)
     (tid : transID) (index : int) (t : Task.task) =
   let id = gen_proofNodeID s in
   let gid,expl,_ = Termcode.goal_expl_task ~root:false t in
   let goal_name = parent_name ^ "." ^ string_of_int index in
   let goal_name = Ident.id_register (Ident.id_derive goal_name gid) in
-  mk_proof_node ~version:s.session_shape_version ~expl
-                s goal_name t (Trans tid) id;
+  mk_new_proof_node ~expl s goal_name t (Trans tid) id;
   id
 
 let mk_transf_node (s : session) (id : proofNodeID) (node_id : transID)
@@ -633,7 +630,7 @@ let graft_transf  (s : session) (id : proofNodeID) (name : string)
     (args : string list) (tl : Task.task list) =
   let tid = gen_transID s in
   let parent_name = (get_proofNode s id).proofn_name.Ident.id_string in
-  let sub_tasks = List.mapi (mk_transf_proof_node s parent_name tid) tl in
+  let sub_tasks = List.mapi (mk_new_transf_proof_node s parent_name tid) tl in
   let proved = sub_tasks = [] in
   mk_transf_node s id tid name args ~proved sub_tasks ~detached:false;
   tid
@@ -1140,7 +1137,6 @@ let build_session (s : session) xml =
   match xml.Xml.name with
   | "why3session" ->
     let shape_version = int_attribute_def "shape_version" xml 1 in
-    s.session_shape_version <- shape_version;
     Debug.dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
     (* just to keep the old_provers somewhere *)
     let old_provers =
@@ -1151,10 +1147,12 @@ let build_session (s : session) xml =
          Debug.dprintf debug "prover %d: %a@." id Whyconf.print_prover p;
          Hprover.replace s.session_prover_ids p id)
       old_provers;
-    Debug.dprintf debug "[Info] load_session: done@\n"
+    Debug.dprintf debug "[Info] load_session: done@\n";
+    shape_version
   | s ->
     Warning.emit "[Warning] Session.load_session: unexpected element '%s'@."
-      s
+                 s;
+    Termcode.current_shape_version
 
 exception ShapesFileError of string
 
@@ -1193,7 +1191,7 @@ let read_sum_and_shape ch =
       | Exit -> Bytes.unsafe_to_string sum, Buffer.contents shape
 
 
-  let use_shapes = ref true
+  let has_shapes = ref true
 
   let fix_attributes ch name attrs =
     if name = "goal" then
@@ -1213,16 +1211,16 @@ let read_sum_and_shape ch =
           with Not_found -> ("sum", sum) :: attrs
         in
         ("shape",shape) :: attrs
-      with _ -> use_shapes := false; attrs
+      with _ -> has_shapes := false; attrs
     else attrs
 
 let read_xml_and_shapes xml_fn compressed_fn =
-  use_shapes := true;
+  has_shapes := true;
   try
     let ch = C.open_in compressed_fn in
     let xml = Xml.from_file ~fixattrs:(fix_attributes ch) xml_fn in
     C.close_in ch;
-    xml, !use_shapes
+    xml, !has_shapes
   with Sys_error msg ->
     raise (ShapesFileError ("cannot open shapes file for reading: " ^ msg))
 end
@@ -1262,18 +1260,18 @@ with e ->
 let load_session (dir : string) =
   let session = empty_session dir in
   let file = Filename.concat dir db_filename in
-  let use_shapes =
+  let shape_version =
     (* If the xml is present we read it, otherwise we consider it empty *)
     if Sys.file_exists file then
       try
 (*
         Termcode.reset_dict ();
 *)
-        let xml,use_shapes =
+        let xml,has_shapes =
           read_file_session_and_shapes dir file in
         try
-          build_session session xml.Xml.content;
-          use_shapes
+          let shape_version = build_session session xml.Xml.content in
+          if has_shapes then Some shape_version else None
         with Sys_error msg ->
           failwith ("Open session: sys error " ^ msg)
       with
@@ -1283,9 +1281,9 @@ let load_session (dir : string) =
       | Xml.Parse_error s ->
         Warning.emit "XML database corrupted, ignored (%s)@." s;
         raise (SessionFileError "XML corrupted")
-    else false
+    else None
   in
-    session, use_shapes
+    session, shape_version
 
 (* -------------------- merge/update session --------------------------- *)
 
@@ -1293,8 +1291,8 @@ let load_session (dir : string) =
 
 module Goal = struct
   type 'a t = proofNodeID * session
-  let checksum (id,s) = Some (get_proofNode s id).proofn_checksum
-  let shape (id,s)    = (get_proofNode s id).proofn_shape
+  let checksum (id,s) = Some (fst (Hpn.find s.session_sum_shape_table id))
+  let shape (id,s)    = snd (Hpn.find s.session_sum_shape_table id)
   let name (id,s)     = (get_proofNode s id).proofn_name
 end
 
@@ -1311,9 +1309,9 @@ let save_detached_proof s parent old_pa_n =
                             parent)
 
 let rec save_detached_goal old_s s parent detached_goal_id id =
-    let detached_goal = get_proofNode old_s detached_goal_id in
-    mk_proof_node_no_task s detached_goal.proofn_name parent id detached_goal.proofn_checksum
-      detached_goal.proofn_shape false;
+  let detached_goal = get_proofNode old_s detached_goal_id in
+  let (sum,shape) = Hpn.find old_s.session_sum_shape_table detached_goal_id in
+    mk_proof_node_no_task s detached_goal.proofn_name parent id sum shape false;
     Hprover.iter (fun _ pa ->
                   let pa = get_proof_attempt_node old_s pa in
                   save_detached_proof s id pa) detached_goal.proofn_attempts;
@@ -1398,19 +1396,19 @@ let add_registered_transformation s env old_tr goal_id =
     in
     graft_transf s goal_id old_tr.transf_name old_tr.transf_args subgoals
 
-let rec merge_goal ~use_shapes env new_s old_s ~goal_obsolete old_goal new_goal_id =
+let rec merge_goal ~shape_version env new_s old_s ~goal_obsolete old_goal new_goal_id =
   Hprover.iter (fun k pa ->
                 let pa = get_proof_attempt_node old_s pa in
                 merge_proof new_s ~goal_obsolete new_goal_id k pa)
                old_goal.proofn_attempts;
   List.iter
-    (merge_trans ~use_shapes env old_s new_s new_goal_id)
+    (merge_trans ~shape_version env old_s new_s new_goal_id)
     old_goal.proofn_transformations;
   let new_goal_node = get_proofNode new_s new_goal_id in
   new_goal_node.proofn_transformations <- List.rev new_goal_node.proofn_transformations;
   update_goal_node (fun _ -> ()) new_s new_goal_id
 
-and merge_trans ~use_shapes env old_s new_s new_goal_id old_tr_id =
+and merge_trans ~shape_version env old_s new_s new_goal_id old_tr_id =
   let old_tr = get_transfNode old_s old_tr_id in
   let old_subtasks = List.map (fun id -> id,old_s)
       old_tr.transf_subtasks in
@@ -1426,12 +1424,13 @@ and merge_trans ~use_shapes env old_s new_s new_goal_id old_tr_id =
     let new_subtasks = List.map (fun id -> id,new_s)
                                 new_tr.transf_subtasks in
     let associated,detached =
-      AssoGoals.associate ~use_shapes old_subtasks new_subtasks
+      AssoGoals.associate ~use_shapes:(shape_version <> None)
+                          old_subtasks new_subtasks
     in
     List.iter
       (function
         | ((new_goal_id,_), Some ((old_goal_id,_), goal_obsolete)) ->
-           merge_goal ~use_shapes env new_s old_s ~goal_obsolete
+           merge_goal ~shape_version env new_s old_s ~goal_obsolete
                       (get_proofNode old_s old_goal_id) new_goal_id
         | ((id,s), None) ->
            Debug.dprintf debug "[merge_trans] missed new subgoal: %s@."
@@ -1459,7 +1458,7 @@ and merge_trans ~use_shapes env old_s new_s new_goal_id old_tr_id =
     exit 2
 
 
-let merge_theory ~use_shapes env old_s old_th s th : unit =
+let merge_theory ~shape_version env old_s old_th s th : unit =
   let get_goal_name goal_node =
     let name = goal_node.proofn_name in
     try
@@ -1481,18 +1480,18 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
          let new_goal = get_proofNode s ng_id in
          (* look for old_goal with matching name *)
          let new_goal_name = get_goal_name new_goal in
-         let old_goal = get_proofNode old_s
-           (Hstr.find old_goals_table new_goal_name) in
+         let old_id = Hstr.find old_goals_table new_goal_name in
+         let old_goal = get_proofNode old_s old_id in
          Hstr.remove old_goals_table new_goal_name;
          let goal_obsolete =
-             let s1 = new_goal.proofn_checksum in
-             let s2 = old_goal.proofn_checksum in
+             let s1 = fst (Hpn.find s.session_sum_shape_table ng_id) in
+             let s2 = fst (Hpn.find old_s.session_sum_shape_table old_id) in
              Debug.dprintf debug "[merge_theory] goal has checksum@.";
              not (Termcode.equal_checksum s1 s2)
          in
          if goal_obsolete then
            found_obsolete := true;
-         merge_goal ~use_shapes env s old_s ~goal_obsolete old_goal ng_id
+         merge_goal ~shape_version env s old_s ~goal_obsolete old_goal ng_id
        with
        | Not_found ->
          (* if no goal of matching name is found store it to look for
@@ -1503,12 +1502,14 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
   (* attach the session to the subtasks to be able to instantiate Pairing *)
   let detached_goals = Hstr.fold (fun _key g tl -> (g,old_s) :: tl) old_goals_table [] in
   let associated,detached =
-    AssoGoals.associate ~use_shapes detached_goals !new_goals
+    AssoGoals.associate ~use_shapes:(shape_version <> None)
+                        detached_goals !new_goals
   in
   List.iter (function
       | ((new_goal_id,_), Some ((old_goal_id,_), goal_obsolete)) ->
         Debug.dprintf debug "[merge_theory] pairing paired one goal, yeah !@.";
-        merge_goal ~use_shapes env s old_s ~goal_obsolete (get_proofNode old_s old_goal_id) new_goal_id
+        merge_goal ~shape_version env s old_s ~goal_obsolete
+                   (get_proofNode old_s old_goal_id) new_goal_id
       | ((id,_), None) ->
          Debug.dprintf debug "[merge_theory] pairing found missed sub goal: %s@."
                        (get_proofNode s id).proofn_name.Ident.id_string;
@@ -1522,10 +1523,16 @@ let merge_theory ~use_shapes env old_s old_th s th : unit =
    provided in merge try to merge the new theory with the previous one *)
 let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theory)
   : theory =
-  let add_goal parent goal id =
-    let name,expl,task = Termcode.goal_expl_task ~root:true goal in
-    mk_proof_node ~version:s.session_shape_version ~expl
-                  s name task parent id;
+  let add_goal =
+    match merge with
+    | Some(_,_,_,Some v) ->
+       fun parent goal id ->
+       let name,expl,task = Termcode.goal_expl_task ~root:true goal in
+       mk_proof_node ~shape_version:v ~expl s name task parent id
+    | _ ->
+       fun parent goal id ->
+       let name,expl,task = Termcode.goal_expl_task ~root:true goal in
+       mk_new_proof_node ~expl s name task parent id
   in
   let tasks = Task.split_theory th None None in
   let goalsID = List.map (fun _ -> gen_proofNodeID s) tasks in
@@ -1538,8 +1545,8 @@ let make_theory_section ?merge ~detached (s:session) parent_name (th:Theory.theo
   List.iter2 (add_goal parent) tasks goalsID;
   begin
     match merge with
-    | Some (old_s, old_th, env, use_shapes) ->
-       merge_theory ~use_shapes env old_s old_th s theory
+    | Some (old_s, old_th, env, shape_version) ->
+       merge_theory ~shape_version env old_s old_th s theory
     | _ -> if tasks <> [] then found_detached := true (* should be found_new_goals instead of found_detached *)
   end;
   theory
@@ -1568,7 +1575,7 @@ let add_file_section (s:session) (fn:string) ~file_is_detached
 
 (* add a why file to a session and try to merge its theories with the
    provided ones with matching names *)
-let merge_file_section ~use_shapes ~old_ses ~old_theories ~file_is_detached ~env
+let merge_file_section ~shape_version ~old_ses ~old_theories ~file_is_detached ~env
     (s:session) (fn:string) (theories:Theory.theory list) format
     : unit =
   Debug.dprintf debug_merge "[Session_itp.merge_file_section] fn = %s@." fn;
@@ -1587,7 +1594,8 @@ let merge_file_section ~use_shapes ~old_ses ~old_theories ~file_is_detached ~env
         let old_th = Hstr.find old_th_table theory_name in
         Debug.dprintf debug_merge "[Session_itp.merge_file_section] theory found: %s@." theory_name;
         Hstr.remove old_th_table theory_name;
-        make_theory_section ~detached:false ~merge:(old_ses,old_th,env,use_shapes) s fn th
+        make_theory_section ~detached:false
+                            ~merge:(old_ses,old_th,env,shape_version) s fn th
       with Not_found ->
         (* if no theory was found we make a new theory section *)
         Debug.dprintf debug_merge "[Session_itp.merge_file_section] theory NOT FOUND in old session: %s@." theory_name;
@@ -1626,31 +1634,56 @@ let read_file env ?format fn =
   in
   List.map (fun (_,_,a) -> a) th
 
-let merge_file  ~use_shapes env (ses : session) (old_ses : session) file =
+let merge_file  ~shape_version env (ses : session) (old_ses : session) file =
   let format = file_format file in
   let old_theories = file_theories file in
   let file_name = Filename.concat (get_dir old_ses) (file_name file) in
   try
     let new_theories = read_file env file_name ?format in
     merge_file_section
-      ses ~use_shapes ~old_ses ~old_theories ~file_is_detached:false
+      ses ~shape_version ~old_ses ~old_theories ~file_is_detached:false
       ~env file_name new_theories format;
     None
   with e -> (* TODO: capture only parsing and typing errors *)
     merge_file_section
-      ses ~use_shapes ~old_ses ~old_theories ~file_is_detached:true
+      ses ~shape_version ~old_ses ~old_theories ~file_is_detached:true
       ~env file_name [] format;
     Some e
 
-let merge_files ~use_shapes env (ses:session)  (old_ses : session) =
+let merge_files ~shape_version env (ses:session)  (old_ses : session) =
   let errors =
     Hstr.fold
       (fun _ f acc ->
-       match merge_file ~use_shapes env ses old_ses f with
+       match merge_file ~shape_version env ses old_ses f with
        | None -> acc
        | Some e -> e :: acc)
       (get_files old_ses) []
   in
+  (* recompute shapes if absent or obsolete *)
+  if shape_version <> Some Termcode.current_shape_version then
+    begin
+      Hpn.clear ses.session_sum_shape_table;
+      let version = Termcode.current_shape_version in
+      fold_all_session
+        ses
+        (fun () n ->
+         match n with
+         | APn id ->
+            let sum,shape =
+              try
+                let t = get_task ses id in
+                let _,expl,_ = Termcode.goal_expl_task ~root:false t in
+                let sum = Termcode.task_checksum ~version t in
+                let shape = Termcode.t_shape_task ~version ~expl t in
+                sum, shape
+              with Not_found -> (* detached goal *)
+                Termcode.dumb_checksum, Termcode.shape_of_string ""
+            in
+            Hpn.add ses.session_sum_shape_table id (sum,shape)
+         | _ -> ()
+        )
+        ()
+    end;
   (errors,!found_obsolete,!found_detached)
 
 
@@ -1659,9 +1692,6 @@ let merge_files ~use_shapes env (ses:session)  (old_ses : session) =
 (************************)
 
 module Mprover = Whyconf.Mprover
-(* dead code
-module Sprover = Whyconf.Sprover
-*)
 module PHprover = Whyconf.Hprover
 
 open Format
@@ -1826,11 +1856,10 @@ let rec save_goal s ctxt fmt pnid =
     save_ident pn.proofn_name
     (save_string_attrib "expl") pn.proofn_expl
     (save_bool_def "proved" false) (pn_proved s pnid);
-  let sum = Termcode.string_of_checksum pn.proofn_checksum in
-  let shape = Termcode.string_of_shape pn.proofn_shape in
-  Compress.Compress_z.output_string ctxt.ch_shapes sum;
+  let (sum,shape) = Hpn.find s.session_sum_shape_table pnid in
+  Compress.Compress_z.output_string ctxt.ch_shapes (Termcode.string_of_checksum sum);
   Compress.Compress_z.output_char ctxt.ch_shapes ' ';
-  Compress.Compress_z.output_string ctxt.ch_shapes shape;
+  Compress.Compress_z.output_string ctxt.ch_shapes (Termcode.string_of_shape shape);
   Compress.Compress_z.output_char ctxt.ch_shapes '\n';
   let l = Hprover.fold
       (fun _ a acc ->
@@ -1888,10 +1917,7 @@ let save fname shfname session =
   fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
   fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"http://why3.lri.fr/why3session.dtd\">@\n";
   fprintf fmt "@[<v 0><why3session shape_version=\"%d\">"
-    session.session_shape_version;
-(*
-  Termcode.reset_dict ();
-*)
+    Termcode.current_shape_version;
   let prover_ids = session.session_prover_ids in
   let provers =
     PHprover.fold (get_prover_to_save prover_ids)
diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli
index 57cee7327c8549f83453be57cd94f2e962bcde13..5d14abdad09f6dfef361736bc205e6bebd7f2a20 100644
--- a/src/session/session_itp.mli
+++ b/src/session/session_itp.mli
@@ -169,8 +169,9 @@ val read_file :
    signaled with exceptions.  *)
 
 val merge_files :
-  use_shapes:bool -> Env.env -> session -> session -> exn list * bool * bool
-(** [merge_files ~use_shapes env ses old_ses] merges the file sections
+  shape_version:int option ->
+  Env.env -> session -> session -> exn list * bool * bool
+(** [merge_files ~use_shape_version env ses old_ses] merges the file sections
     of session [s] with file sections of the same name in old session
     [old_ses]. Recursively, for each theory whose name is identical to
     old theories, it is attempted to associate the old goals,
@@ -221,11 +222,11 @@ val mark_obsolete: session -> proofAttemptID -> unit
 val save_session : session -> unit
 (** [save_session s] Save the session [s] *)
 
-val load_session : string -> session * bool
+val load_session : string -> session * int option
 (** [load_session dir] load a session in directory [dir]; all the
     tasks are initialised to None
 
-    The returned boolean is set when there was shapes read from disk.
+    The second result is the shape version read from disk, if any
 
     raises [SessionFileError msg] if the database file cannot be read
     correctly.
diff --git a/src/tools/why3replay.ml b/src/tools/why3replay.ml
index 93b8b6e0eba7d0b9d1a75c70786f0650c78e18bd..e9a72f973ad7f8973e8464a937b3b19a4845ce26 100644
--- a/src/tools/why3replay.ml
+++ b/src/tools/why3replay.ml
@@ -384,12 +384,12 @@ let () =
     Whyconf.Args.exit_with_usage option_list usage_msg;
   try
     Debug.dprintf debug "Opening session '%s'...@?" dir;
-    let ses,use_shapes = S.load_session dir in
+    let ses,shape_version = S.load_session dir in
     let cont = Controller_itp.create_controller config env ses in
     (* update the session *)
     let found_obs, found_detached =
       try
-        Controller_itp.reload_files cont ~use_shapes
+        Controller_itp.reload_files cont ~shape_version
       with
       | Controller_itp.Errors_list l ->
           List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
diff --git a/src/why3session/why3session_lib.ml b/src/why3session/why3session_lib.ml
index df5c61b3d47c53f1c857c52f543e2ff2b9ff81bf..b46b473928528dfb09d1187f178bd1ebc178d72f 100644
--- a/src/why3session/why3session_lib.ml
+++ b/src/why3session/why3session_lib.ml
@@ -78,7 +78,7 @@ let read_session fname =
   S.load_session project_dir
 
 let read_update_session ~allow_obsolete env config fname =
-  let session,use_shapes = read_session fname in
+  let session,shape_version = read_session fname in
 (*
   let ctxt = S.mk_update_context
     ~allow_obsolete_goals:allow_obsolete
@@ -90,7 +90,7 @@ let read_update_session ~allow_obsolete env config fname =
   let cont = Controller_itp.create_controller config env session in
   let found_obs, some_merge_miss =
     try
-      Controller_itp.reload_files cont ~use_shapes
+      Controller_itp.reload_files cont ~shape_version
     with
     | Controller_itp.Errors_list l ->
         List.iter (fun e -> Format.eprintf "%a@." Exn_printer.exn_printer e) l;
diff --git a/src/why3session/why3session_lib.mli b/src/why3session/why3session_lib.mli
index 951f4398e742761b24e142c91634967c46730e97..1e2c4ab031844e61d51f69bb614a5609c14183ff 100644
--- a/src/why3session/why3session_lib.mli
+++ b/src/why3session/why3session_lib.mli
@@ -44,7 +44,10 @@ val common_options : spec_list
 val read_env_spec : unit -> Env.env * Whyconf.config * bool
 (** read_simple_spec also *)
 
-val read_session : string -> Session_itp.session * bool
+val read_session : string -> Session_itp.session * int option
+(** [read_session s] reads the session file [s] and returns a pair
+[(ses,shape_version)] where [ses] is the session structure (without
+any tasks) and [shape_version] indicates the shapes version, if any *)
 
 val read_update_session :
   allow_obsolete:bool -> Env.env ->