Merge PR#676: Primitive Ltac definitions for first and solve

2 files changed, 50 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 0346c4a555..bb679ecba7 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -522,6 +522,19 @@ to have \emph{at least} one success.
 
 \ErrMsg \errindex{No applicable tactic}
 
+\variant {\tt first {\tacexpr}}
+
+This is an Ltac alias that gives a primitive access to the {\tt first} tactical
+as a Ltac definition without going through a parsing rule. It expects to be
+given a list of tactics through a {\tt Tactic Notation}, allowing to write
+notations of the following form.
+
+\Example
+
+\begin{quote}
+{\tt Tactic Notation "{foo}" tactic\_list(tacs) := first tacs.}
+\end{quote}
+
 \subsubsection[Left-biased branching]{Left-biased branching\tacindex{$\mid\mid$}
 \index{Tacticals!orelse@{\tt $\mid\mid$}}}
 
@@ -600,6 +613,11 @@ $v_2$ and so on. It fails if there is no solving tactic.
 
 \ErrMsg \errindex{Cannot solve the goal}
 
+\variant {\tt solve {\tacexpr}}
+
+This is an Ltac alias that gives a primitive access to the {\tt solve} tactical.
+See the {\tt first} tactical for more information.
+
 \subsubsection[Identity]{Identity\label{ltac:idtac}\tacindex{idtac}
 \index{Tacticals!idtac@{\tt idtac}}}
 
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 6890b31981..0a13a20a97 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -326,3 +326,35 @@ let initial_atomic () =
       ]
 
 let () = Mltop.declare_cache_obj initial_atomic "coretactics"
+
+(* First-class Ltac access to primitive blocks *)
+
+let initial_name s = { mltac_plugin = "coretactics"; mltac_tactic = s; }
+let initial_entry s = { mltac_name = initial_name s; mltac_index = 0; }
+
+let register_list_tactical name f =
+  let tac args ist = match args with
+  | [v] ->
+    begin match Tacinterp.Value.to_list v with
+    | None -> Tacticals.New.tclZEROMSG (Pp.str "Expected a list")
+    | Some tacs ->
+      let tacs = List.map (fun tac -> Tacinterp.tactic_of_value ist tac) tacs in
+      f tacs
+    end
+  | _ -> assert false
+  in
+  Tacenv.register_ml_tactic (initial_name name) [|tac|]
+
+let () = register_list_tactical "first" Tacticals.New.tclFIRST
+let () = register_list_tactical "solve" Tacticals.New.tclSOLVE
+
+let initial_tacticals () =
+  let idn n = Id.of_string (Printf.sprintf "_%i" n) in
+  let varn n = Reference (ArgVar (None, idn n)) in
+  let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
+  List.iter iter [
+    "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0])));
+    "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
+  ]
+
+let () = Mltop.declare_cache_obj initial_tacticals "coretactics"