diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index bb9af717ec9694aaf30726bea30a0880729e21cb..ef36ce6af08ad80830385d2fbcf1aa90934b2b5f 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -30,6 +30,7 @@ type node = {
   parent : node option ;
   mutable script : script ;
   mutable stats : Stats.stats ;
+  mutable strategy : string option ; (* hint *)
   mutable search_index : int ;
   mutable search_space : Strategy.t array ; (* sorted by priority *)
 }
@@ -98,6 +99,7 @@ let proof ~main =
 let rec reset_node n =
   Wpo.clear_results n.goal ;
   if Wpo.is_tactic n.goal then Wpo.remove n.goal ;
+  n.strategy <- None ;
   match n.script with
   | Opened | Script _ -> ()
   | Tactic(_,children) -> iter_all reset_node children
@@ -325,6 +327,7 @@ let mk_tree_node ~tree ~anchor goal = {
   stats = Stats.empty ;
   search_index = 0 ;
   search_space = [| |] ;
+  strategy = None ;
 }
 
 let mk_root_node goal = {
@@ -332,6 +335,7 @@ let mk_root_node goal = {
   parent = None ;
   script = Opened ;
   stats = Stats.empty ;
+  strategy = None ;
   search_index = 0 ;
   search_space = [| |] ;
 }
@@ -437,4 +441,7 @@ let bound node =
   | Tactic _ | Opened -> []
   | Script s -> s
 
+let get_hint node = node.strategy
+let set_hint node strategy = node.strategy <- Some strategy
+
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index f009fd7c28e25542be4abe43461ce0ff13f8a7ae..81f682d62f62315225dc83dd4add8ccca77773a1 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -77,6 +77,9 @@ val children : node -> (string * node) list
 val tactical : node -> ProofScript.jtactic option
 val get_strategies : node -> int * Strategy.t array (* current index *)
 val set_strategies : node -> ?index:int -> Strategy.t array -> unit
+val get_hint : node -> string option
+val set_hint : node -> string -> unit
+
 val forward : tree -> unit
 val cancel : tree -> unit
 
diff --git a/src/plugins/wp/ProofStrategy.ml b/src/plugins/wp/ProofStrategy.ml
index 0bed5346b2cb39beffe1fa05fc60733825c91161..9112e292372396937b661ec9f607ce64d081d941 100644
--- a/src/plugins/wp/ProofStrategy.ml
+++ b/src/plugins/wp/ProofStrategy.ml
@@ -378,7 +378,22 @@ let configure tactic sigma (a,v) =
         raise Not_found
     end
 
-let tactic tree node = function
+let subgoal (children : (string loc * string loc) list)
+    (default : string loc option) (goal,node) =
+  let hint = List.find_map (fun (g,s) ->
+      if String.starts_with ~prefix:g.value goal then Some s else None
+    ) children in
+  begin
+    match hint, default with
+    | None, None -> ()
+    | Some s , _ | None , Some s ->
+      if not @@ Strategies.mem s.value then
+        Wp_parameters.error ~source:(fst s.loc)
+          "Unknown strategy '%s' (skipped)" s.value
+      else ProofEngine.set_hint node s.value
+  end ; node
+
+let tactic tree node strategy = function
   | Strategy _ | Auto _ | Provers _ -> None
   | Tactic t ->
     try
@@ -388,16 +403,19 @@ let tactic tree node = function
       let ctxt = ProofEngine.node_context node in
       let sequent = snd @@ Wpo.compute @@ ProofEngine.goal node in
       let console = new ProofScript.console ~pool ~title in
-      let children = WpContext.on_context ctxt
+      let subgoals = WpContext.on_context ctxt
           begin fun () ->
             let sigma = bind Pattern.empty sequent t.lookup in
             List.iter (configure tactic sigma) t.params ;
             let selection = select sigma t.select in
             match tactic#select console selection with
-            | exception _ | Not_applicable ->
-              Wp_parameters.error ~source:(fst t.tactic.loc)
-                "Tactical '%s' not applicable on selection@ (%a)"
-                t.tactic.value Tactical.pp_selection selection ;
+            | exception (Not_found | Exit) -> raise Not_found
+            | Not_applicable ->
+              raise Not_found
+            | exception exn when Wp_parameters.protect exn ->
+              Wp_parameters.warning ~source:(fst t.tactic.loc)
+                "Tactical '%s' configuration error (%s)"
+                t.tactic.value (Printexc.to_string exn) ;
               raise Not_found
             | Not_configured ->
               Wp_parameters.error ~source:(fst t.tactic.loc)
@@ -405,13 +423,12 @@ let tactic tree node = function
                 t.tactic.value ;
               raise Not_found
             | Applicable process ->
-              let script = ProofScript.jtactic tactic selection in
+              let strategy = strategy.name.value in
+              let script = ProofScript.jtactic ~strategy tactic selection in
               let fork = ProofEngine.fork tree ~anchor:node script process in
               snd @@ ProofEngine.commit fork
-          end ()
-      in Some children
+          end () in
+      Some (List.map (subgoal t.children t.default) subgoals)
     with Not_found -> None
 
-let () = ignore tactic
-
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofStrategy.mli b/src/plugins/wp/ProofStrategy.mli
index c16b9648e4b9a5eb9f7bb0fc373b7a177e1b102d..ea8b19ec6acd8f52271ce60b3ec83d178a2fab4a 100644
--- a/src/plugins/wp/ProofStrategy.mli
+++ b/src/plugins/wp/ProofStrategy.mli
@@ -20,6 +20,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open ProofEngine
+
 (* -------------------------------------------------------------------------- *)
 (* --- Proof Strategy Engine                                              --- *)
 (* -------------------------------------------------------------------------- *)
@@ -34,5 +36,6 @@ val hints : WpPropId.prop_id -> strategy list
 val alternatives : strategy -> alternative list
 val provers : alternative -> VCS.prover list * float
 val fallback : alternative -> strategy option
+val tactic : tree -> node -> strategy -> alternative -> node list option
 
 (* -------------------------------------------------------------------------- *)