update remaining uses of deprecated transformation split_goal_wp

src/driver/whyconf.ml

@@ -144,26 +144,6 @@ type config_strategy = {
   strategy_shortcut : string;
 }
 
-(* a default set of strategies *)
-(*
-let default_strategies =
-  List.map
-    (fun (name,desc,shortcut,code) ->
-      let s = ref Rc.empty_section in
-      s := Rc.set_string !s "name" name;
-      s := Rc.set_string !s "desc" desc;
-      s := Rc.set_string !s "shortcut" shortcut;
-      s := Rc.set_string !s "code" code;
-      !s)
-    [ "Split", "Split@ conjunctions@ in@ goal", "s",
-      "t split_goal_wp exit";
-      "Inline", "Inline@ function@ symbols@ once", "i",
-      "t inline_goal exit";
-      "Compute", "Compute@ in@ goal", "c",
-      "t compute_in_goal exit";
-    ]
- *)
-
 let get_strategies ?(default=[]) rc =
   match get_simple_family rc "strategy" with
     | [] -> default

src/transform/introduction.ml

@@ -76,14 +76,6 @@ let () = Trans.register_transform "introduce_premises" introduce_premises
   ~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \
          goal@ into@ constant@ symbol@ and@ axioms."
 
-(*
-let split_intro =
-  Trans.compose_l Split_goal.split_goal_wp (Trans.singleton introduce_premises)
-
-let () = Trans.register_transform_l "split_intro" split_intro
-  ~desc:"Same@ as@ split_goal_wp,@ but@ moves@ \
-    the@ implication@ antecedents@ to@ premises."
- *)
 
 (** Destruction of existential quantifiers in axioms.
     Contributed by Nicolas Jeannerod [niols@niols.fr] *)

src/trywhy3/why3_worker.ml

@@ -56,8 +56,7 @@ let alt_ergo_driver : Driver.driver =
 
 let () = log_time ("Initialising why3 worker: end ")
 
-let split_trans = Trans.lookup_transform_l "split_goal_wp" env
-let intro_trans = Trans.lookup_transform "introduce_premises" env
+let split_trans = Trans.lookup_transform_l "split_intros_goal_wp" env
 
 (* CF gmain.ml ligne 568 et suivante *)
 module W =
@@ -175,7 +174,7 @@ module Task =
 	  subtasks = [];
 	  loc = id_loc @  (collect_locs task);
 	  expl = expl;
-          pretty = task_text (Trans.apply intro_trans task);
+          pretty = task_text task;
         }
       in
       Hashtbl.add task_table id task_info;