From fb9815baafc008a6e67e542eb8c2adf7a6375fe8 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 19 Dec 2014 10:28:58 +0100
Subject: 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.
---
 intf/tacexpr.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'intf')

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 *)
-- 
cgit v1.2.3