diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index b0d374a7456fd0177fc814cc48f36a0396c60ec8..9d72711ea9a3418a8296e644c75ca2fc30377fe2 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -281,14 +281,16 @@ type jtactic = {
   tactic : string ;
   params : Json.t ;
   select : Json.t ;
+  strategy : string option ;
 }
 
-let jtactic (tac : tactical) (sel : selection) =
+let jtactic ?strategy (tac : tactical) (sel : selection) =
   {
     header = tac#title ;
     tactic = tac#id ;
     params = json_of_parameters tac ;
     select = json_of_selection sel ;
+    strategy = Option.map ProofStrategy.name strategy ;
   }
 
 let json_of_tactic t js =
@@ -314,8 +316,11 @@ let tactic_of_json js =
     let tactic = js >? "tactic" |> Json.string in
     let params = try js >? "params" with Not_found -> `Null in
     let select = try js >? "select" with Not_found -> `Null in
-    let children = try js >? "children" |> children_of_json with Not_found -> [] in
-    Some( { header ; tactic ; params ; select } , children )
+    let children =
+      try js >? "children" |> children_of_json with Not_found -> [] in
+    let strategy =
+      try Some (js >? "strategy" |> Json.string) with Not_found -> None in
+    Some( { header ; tactic ; params ; select ; strategy } , children )
   with _ -> None
 
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofScript.mli b/src/plugins/wp/ProofScript.mli
index eb368c02225fd923c6399488bed99699f091ee92..7fe27cbb04d87de398b0cd1e56eb2485194ff8ed 100644
--- a/src/plugins/wp/ProofScript.mli
+++ b/src/plugins/wp/ProofScript.mli
@@ -35,6 +35,7 @@ and jtactic = {
   tactic : string ;
   params : Json.t ;
   select : Json.t ;
+  strategy : string option ;
 }
 
 val is_prover : alternative -> bool
@@ -54,7 +55,7 @@ val has_proof : jscript -> bool
 val decode : Json.t -> jscript
 val encode : jscript -> Json.t
 
-val jtactic : tactical -> selection -> jtactic
+val jtactic : ?strategy:ProofStrategy.strategy -> tactical -> selection -> jtactic
 val configure : jtactic -> sequent -> (tactical * selection) option
 
 (** Json Codecs *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 12cd19f184c9da91c2ca9aa63006c5eabece1d51..4b246d88518f70abd66bf8193b8000f2f7b3577f 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -340,13 +340,13 @@ let rec crawl env on_child node = function
     if ok then Env.validate env else Env.stuck env ;
     Task.return ()
 
-  | Error(msg,json) :: alternative ->
+  | Error(msg,json) :: alternatives ->
     Wp_parameters.warning "@[<hov 2>Script Error: on goal %a@\n%S: %a@]@."
       WpPropId.pretty (Env.goal env node).po_pid
       msg Json.pp json ;
-    crawl env on_child node alternative
+    crawl env on_child node alternatives
 
-  | Prover( prv , res ) :: alternative ->
+  | Prover( prv , res ) :: alternatives ->
     begin
       let task =
         if Env.play env prv res then
@@ -357,12 +357,12 @@ let rec crawl env on_child node = function
       let continue ok =
         if ok
         then (Env.validate env ; Task.return ())
-        else crawl env on_child node alternative
+        else crawl env on_child node alternatives
       in
       task >>= continue
     end
 
-  | Tactic( _ , jtactic , subscripts ) :: alternative ->
+  | Tactic( _ , jtactic , subscripts ) :: alternatives ->
     begin
       try
         let residual = apply env node jtactic subscripts in
@@ -383,7 +383,12 @@ let rec crawl env on_child node = function
           (Printexc.to_string exn)
           Json.pp jtactic.params
           Json.pp jtactic.select ;
-        crawl env on_child node alternative
+        match jtactic.strategy with
+        | None -> crawl env on_child node alternatives
+        | Some s ->
+          (*TODO TRY STRATEGY FIRST *)
+          ignore s ;
+          crawl env on_child node alternatives
     end
 
 (* -------------------------------------------------------------------------- *)