Another batch of primitive operations.

5 files changed, 58 insertions, 5 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index 9bc7107cc7..695fc7d430 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -97,13 +97,13 @@ GEXTEND Gram
     ]
   ;
   tac2expr:
-    [ "top" RIGHTA
+    [ "6" RIGHTA
         [ e1 = SELF; ";"; e2 = SELF -> CTacSeq (!@loc, e1, e2) ]
     | "5"
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "top" -> CTacFun (!@loc, it, body)
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "6" -> CTacFun (!@loc, it, body)
       | "let"; isrec = rec_flag;
           lc = LIST1 let_clause SEP "with"; "in";
-          e = tac2expr LEVEL "top" -> CTacLet (!@loc, isrec, lc, e)
+          e = tac2expr LEVEL "6" -> CTacLet (!@loc, isrec, lc, e)
       | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches; "end" ->
          CTacCse (!@loc, e, bl)
       ]
@@ -135,7 +135,7 @@ GEXTEND Gram
   ]
   ;
   branch:
-  [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "top" -> (pat, e) ] ]
+  [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "6" -> (pat, e) ] ]
   ;
   rec_flag:
     [ [ IDENT "rec" -> true
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 08f61f2c6c..1c03cc410d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -877,7 +877,7 @@ let () = add_scope "tactic" begin function
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
 | [SexprInt (loc, n)] ->
-  let () = if n < 0 || n > 5 then scope_fail () in
+  let () = if n < 0 || n > 6 then scope_fail () in
   let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in
   let act tac = tac in
   Tac2entries.ScopeRule (scope, act)
diff --git a/tests/tacticals.v b/tests/tacticals.v
new file mode 100644
index 0000000000..73f9c03b87
--- /dev/null
+++ b/tests/tacticals.v
@@ -0,0 +1,22 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+Goal True.
+Proof.
+Fail fail.
+Fail solve [ () ].
+try fail.
+repeat fail.
+repeat ().
+solve [ constructor ].
+Qed.
+
+Goal True.
+Proof.
+first [
+  Message.print (Message.of_string "Yay"); fail
+| constructor
+| Message.print (Message.of_string "I won't be printed")
+].
+Qed.
diff --git a/theories/Init.v b/theories/Init.v
index 803e48e352..1591747eb4 100644
--- a/theories/Init.v
+++ b/theories/Init.v
@@ -60,3 +60,6 @@ Ltac2 Type exn ::= [ Not_found ].
 
 Ltac2 Type exn ::= [ Match_failure ].
 (** Used to signal a pattern didn't match a term. *)
+
+Ltac2 Type exn ::= [ Tactic_failure ].
+(** Generic error for tactic failure. *)
diff --git a/theories/Notations.v b/theories/Notations.v
index 0fa3456196..97f3042d2b 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -27,6 +27,10 @@ match Control.case t with
   Control.plus (fun _ => s x) (fun e => s (k e))
 end.
 
+Ltac2 fail0 (_ : unit) := Control.zero Tactic_failure.
+
+Ltac2 Notation fail := fail0 ().
+
 Ltac2 try0 t := Control.enter (fun _ => orelse t (fun _ => ())).
 
 Ltac2 Notation try := try0.
@@ -53,6 +57,28 @@ Ltac2 progress0 tac := Control.enter (fun _ => Control.progress tac).
 
 Ltac2 Notation progress := progress0.
 
+Ltac2 rec first0 tacs :=
+match tacs with
+| [] => Control.zero Tactic_failure
+| tac :: tacs => Control.enter (fun _ => orelse tac (fun _ => first0 tacs))
+end.
+
+Ltac2 Notation "first" "[" tacs(list0(thunk(tactic(6)), "|")) "]" := first0 tacs.
+
+Ltac2 complete tac :=
+  let ans := tac () in
+  Control.enter (fun () => Control.zero Tactic_failure);
+  ans.
+
+Ltac2 rec solve0 tacs :=
+match tacs with
+| [] => Control.zero Tactic_failure
+| tac :: tacs =>
+  Control.enter (fun _ => orelse (fun _ => complete tac) (fun _ => first0 tacs))
+end.
+
+Ltac2 Notation "solve" "[" tacs(list0(thunk(tactic(6)), "|")) "]" := solve0 tacs.
+
 Ltac2 time0 tac := Control.time None tac.
 
 Ltac2 Notation time := time0.
@@ -254,3 +280,5 @@ Ltac2 Notation etransitivity := Std.etransitivity ().
 Ltac2 Notation admit := Std.admit ().
 
 Ltac2 Notation clear := Std.keep [].
+
+Ltac2 Notation refine := Control.refine.