[wp] -wp-auto fallback in strategies

src/plugins/wp/ProofStrategy.ml

@@ -42,6 +42,7 @@ type strategy = {
 and alternative =
   | Strategy of string loc
   | Provers of string loc list * float option (* timeout *)
+  | Auto of string loc list (* deprecated -wp-auto *)
   | Tactic of {
       tactic : string loc ;
       select : value list ;
@@ -193,6 +194,9 @@ let parse_alternative ctxt p =
     let tactic = parse_name ctxt ~kind:"tactic" p in
     parse_tactic_params ctxt (Pattern.context ctxt) ~tactic
       ~select:[] ~lookup:[] ~params:[] ~children:[] ~default:None ps
+  | PLapp("\\auto",[],ps) ->
+    let strategies = List.map (parse_name ctxt ~kind:"auto") ps in
+    Auto strategies
   | _ -> ctxt.error loc "Strategy definition expected (%a)" debug p
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/doc/manual/wp_plugin.tex

@@ -1686,6 +1686,7 @@ Strategy consists of list of alternatives with the following syntax:
     \textit{alternative} $::=$ \\
     \quad$|$\quad\verb+\prover+(\verb+"p"+\pdots\verb+"p"+, \textit{timeout}) \\
     \quad$|$\quad\verb+\tactic+(\verb+"id"+, \textit{param}\pdots\textit{param}) \\
+    \quad$|$\quad\verb+\auto+(\verb+"id"+,\pdots\verb+"id"+) \\
     \quad$|$\quad\verb+\default+ \\
     \quad$|$\quad\textit{strategy}
   \end{tabular}
@@ -1702,6 +1703,8 @@ Each form \emph{alternative} consists of one possible solution to discharge a pr
 \item \verb+\tactic(id,prm...)+ will try to apply the specified tactic with the
   associated parameters. Tactic parameters allows to select the target of the tactic,
   and the strategy to be used on generated sub-goals.
+\item \verb+\auto(id,...)+ will try to apply the (deprecated) auto-strategies
+  available in \textsf{WP} versions prior to Cobalt.
 \item \textit{name} or \verb$\default$ tries the specified strategy.
 \end{itemize}