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.
---
 grammar/q_coqast.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index e3d910f321..c7d126c37d 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -291,7 +291,7 @@ let mlexpr_of_entry_type = function
 
 let mlexpr_of_match_lazy_flag = function
   | Tacexpr.General -> <:expr<Tacexpr.General>>
-  | Tacexpr.Lazy    -> <:expr<Tacexpr.Lazy>>
+  | Tacexpr.Select    -> <:expr<Tacexpr.Select>>
   | Tacexpr.Once    -> <:expr<Tacexpr.Once>>
 
 let mlexpr_of_match_pattern = function
-- 
cgit v1.2.3