Passing an optional message to Tactic_failure.

3 files changed, 6 insertions, 6 deletions

diff --git a/tests/errors.v b/tests/errors.v
index e7beff3420..c677f6af5d 100644
--- a/tests/errors.v
+++ b/tests/errors.v
@@ -7,6 +7,6 @@ let x := Control.plus
   (fun e => match e with Not_found => 1 | _ => 2 end) in
 match Int.equal x 2 with
 | true => ()
-| false => Control.throw Tactic_failure
+| false => Control.throw (Tactic_failure None)
 end.
 Abort.
diff --git a/theories/Init.v b/theories/Init.v
index baaf5956b2..04394e2c5d 100644
--- a/theories/Init.v
+++ b/theories/Init.v
@@ -67,5 +67,5 @@ 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 ].
+Ltac2 Type exn ::= [ Tactic_failure (message option) ].
 (** Generic error for tactic failure. *)
diff --git a/theories/Notations.v b/theories/Notations.v
index 46c0e5e79f..411367eab1 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -27,7 +27,7 @@ match Control.case t with
   Control.plus (fun _ => s x) (fun e => s (k e))
 end.
 
-Ltac2 fail0 (_ : unit) := Control.enter (fun _ => Control.zero Tactic_failure).
+Ltac2 fail0 (_ : unit) := Control.enter (fun _ => Control.zero (Tactic_failure None)).
 
 Ltac2 Notation fail := fail0 ().
 
@@ -69,7 +69,7 @@ Ltac2 Notation progress := progress0.
 
 Ltac2 rec first0 tacs :=
 match tacs with
-| [] => Control.zero Tactic_failure
+| [] => Control.zero (Tactic_failure None)
 | tac :: tacs => Control.enter (fun _ => orelse tac (fun _ => first0 tacs))
 end.
 
@@ -77,12 +77,12 @@ Ltac2 Notation "first" "[" tacs(list0(thunk(tactic(6)), "|")) "]" := first0 tacs
 
 Ltac2 complete tac :=
   let ans := tac () in
-  Control.enter (fun () => Control.zero Tactic_failure);
+  Control.enter (fun () => Control.zero (Tactic_failure None));
   ans.
 
 Ltac2 rec solve0 tacs :=
 match tacs with
-| [] => Control.zero Tactic_failure
+| [] => Control.zero (Tactic_failure None)
 | tac :: tacs =>
   Control.enter (fun _ => orelse (fun _ => complete tac) (fun _ => solve0 tacs))
 end.