Fixed small bug due to previous cleaning. Better cleaning in fact!

src/ide/gmain.ml

@@ -812,7 +812,7 @@ let sched =
     Debug.dprintf debug "@[<hov 2>[GUI session] Opening session...@\n";
     let session,use_shapes =
       if Sys.file_exists project_dir then
-        S.read_session ~keygen:MA.create project_dir
+        S.read_session project_dir
       else
         S.create_session project_dir, false
     in

src/session/session.ml

@@ -1600,7 +1600,7 @@ with e ->
     (Printexc.to_string e);
   Xml.from_file xml_filename, false
 
-let read_session ~keygen dir =
+let read_session_with_keys ~keygen dir =
   if not (Sys.file_exists dir && Sys.is_directory dir) then
     raise (SessionFileError (Pp.sprintf "%s is not an existing directory" dir));
   let xml_filename = Filename.concat dir db_filename in
@@ -1627,7 +1627,7 @@ let read_session ~keygen dir =
   in
   session, use_shapes
 
-let read_session_no_keys = read_session ~keygen:(fun ?parent:_ () -> ())
+let read_session = read_session_with_keys ~keygen:(fun ?parent:_ () -> ())
 
 (*******************************)
 (* Session modification        *)
@@ -2337,8 +2337,11 @@ and merge_trans ~ctxt ~theories env to_goal _ from_transf =
       | (_, None) ->
         found_missed_goals_in_theory := true)
       associated;
+(* TODO: we should copy the goal, using the new new type of keys
     if detached <> [] then
     to_transf.transf_detached <- Some { detached_goals = detached }
+ *)
+    ignore detached
   with Exit -> ()
 
 (** convert the ident from the old task to the ident at the same
@@ -2670,8 +2673,11 @@ and add_transf_to_goal ~keygen env to_goal from_transf =
     add_goal_to_parent ~keygen env from_goal to_goal
   | (_, None) -> ()
   ) associated;
+(*
   if detached <> [] then
     to_transf.transf_detached <- Some { detached_goals = detached };
+ *)
+  ignore(detached);
   to_transf
 
 let get_project_dir fname =

src/session/session.mli

@@ -191,7 +191,7 @@ type 'key keygen = ?parent:'key -> unit -> 'key
 exception ShapesFileError of string
 exception SessionFileError of string
 
-val read_session : keygen:'key keygen -> string -> 'key session * bool
+val read_session: string -> unit session * bool
 (** Read a session stored on the disk. It returns a session without any
     task attached to goals.
 
@@ -205,7 +205,6 @@ val read_session : keygen:'key keygen -> string -> 'key session * bool
 
 *)
 
-val read_session_no_keys: string -> unit session * bool
 
 val save_session : Whyconf.config -> 'key session -> unit
 (** Save a session on disk *)
@@ -250,7 +249,7 @@ type 'key update_context =
     keygen : 'key keygen;
   }
 
-val update_session : ctxt:'key update_context -> 'key session ->
+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

src/session/session_scheduler.mli

@@ -113,7 +113,7 @@ module Make(O: OBSERVER) : sig
     allow_obsolete:bool ->
     release:bool ->
     use_shapes:bool ->
-    O.key session ->
+    'oldkey session ->
     Env.env -> Whyconf.config ->
     O.key env_session * bool * bool
   (**

src/tools/why3replay.ml

@@ -401,7 +401,7 @@ let () =
     Debug.dprintf debug "Opening session...@?";
     O.verbose := Debug.test_flag debug;
     let env_session,found_obs,some_merge_miss =
-      let session, use_shapes = S.read_session ~keygen:O.create project_dir in
+      let session, use_shapes = S.read_session project_dir in
       M.update_session ~allow_obsolete:true ~release:false ~use_shapes
         session env config
     in

src/why3session/why3session_csv.ml

@@ -117,7 +117,7 @@ let rec print_line fmt provers a =
 
 let run_one_normal filter_provers fmt fname =
   let project_dir = Session.get_project_dir fname in
-  let session,_use_shapes = Session.read_session_no_keys project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let provers = Session.get_used_provers session in
   let provers =
     match filter_provers with
@@ -168,7 +168,7 @@ let grab_valid_time provers_time provers pa =
 
 let run_one_by_time provers_time filter_provers fname =
   let project_dir = Session.get_project_dir fname in
-  let session,_use_shapes = Session.read_session_no_keys project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let provers = Session.get_used_provers session in
   let provers =
     match filter_provers with

src/why3session/why3session_html.ml

@@ -71,7 +71,7 @@ type context =
 
 let run_file (context : context) print_session fname =
   let project_dir = Session.get_project_dir fname in
-  let session,_use_shapes = Session.read_session_no_keys project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let output_dir =
     if !output_dir = "" then project_dir else !output_dir
   in

src/why3session/why3session_info.ml

@@ -354,7 +354,7 @@ let print_stats r0 r1 stats =
 let run_one stats r0 r1 fname =
   let project_dir = Session.get_project_dir fname in
   if !opt_project_dir then printf "%s@." project_dir;
-  let session,_use_shapes = Session.read_session_no_keys project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let sep = if !opt_print0 then Pp.print0 else Pp.newline in
   if !opt_print_provers then
     printf "%a@."

src/why3session/why3session_latex.ml

@@ -456,7 +456,7 @@ let table () = if !opt_longtable then "longtable" else "tabular"
 
 let run_one fname =
   let project_dir = Session.get_project_dir fname in
-  let session,_use_shapes = Session.read_session_no_keys project_dir in
+  let session,_use_shapes = Session.read_session project_dir in
   let dir = if !opt_output_dir = "" then project_dir else
       !opt_output_dir
   in

src/why3session/why3session_lib.ml

@@ -73,7 +73,7 @@ let read_env_spec () =
 
 let read_update_session ~allow_obsolete env config fname =
   let project_dir = S.get_project_dir fname in
-  let session,use_shapes = S.read_session_no_keys project_dir in
+  let session,use_shapes = S.read_session project_dir in
   let ctxt = {
     S.allow_obsolete_goals = allow_obsolete;
     S.release_tasks = false;

tests/test_merge.mlw

@@ -8,4 +8,6 @@ theory T
 
   goal g: p 3 /\ p 4 /\ p 5
 
+  goal h : false
+
 end
\ No newline at end of file