From 2a0a48834f0b90319e56ae9f4a172fe6855583c0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 1 Sep 2017 00:19:33 +0200
Subject: Passing an optional message to Tactic_failure.

---
 tests/errors.v       | 2 +-
 theories/Init.v      | 2 +-
 theories/Notations.v | 8 ++++----
 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.
-- 
cgit v1.2.3