From 239fe70ae8a39f5c5619cf88f1ae264c31bda65e Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Dec 2014 13:27:10 +0100
Subject: Fix compilation error in some configurations.

This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select".

Fixes #3877.
---
 intf/tacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7c898b75eb..c4e91d32ee 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -22,7 +22,7 @@ open Locus
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag =
   | General (* returns all possible successes *)
-  | Lazy    (* returns all successes of the first matching branch *)
+  | Select  (* 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 *)
-- 
cgit v1.2.3