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.
---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a8da8c81f5..a088070342 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1559,7 +1559,7 @@ and interp_match_successes lz ist s =
     match lz with
     | General ->
         general
-    | Lazy ->
+    | Select ->
       begin
         (** Only keep the first matching result, we don't backtrack on it *)
         let s = Proofview.tclONCE s in
-- 
cgit v1.2.3