Add a backtracking version of Ltac's [match].

[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.

1 files changed, 5 insertions, 1 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 0c2b754788..7c898b75eb 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -20,7 +20,11 @@ open Misctypes
 open Locus
 
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
-type lazy_flag = bool      (* true = lazy             false = eager *)
+type lazy_flag =
+  | General (* returns all possible successes *)
+  | Lazy    (* returns all successes of the first matching branch *)
+  | Once    (* returns the first success in a maching branch
+               (not necessarily the first) *)
 type evars_flag = bool     (* true = pose evars       false = fail on evars *)
 type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)