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

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index ddb85a3626..ac06bb39f3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -623,7 +623,7 @@ module Make
 
   let pr_lazy = function
     | General -> keyword "multi"
-    | Lazy -> keyword "lazy"
+    | Select -> keyword "lazy"
     | Once -> mt ()
 
   let pr_match_pattern pr_pat = function
-- 
cgit v1.2.3