From fb59652405d0e6a9d1100142d473374cd82ae16b Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 16 Dec 2013 17:30:30 +0100
Subject: Get rid of messages "emitting ..." when compiling .v files

 If these messages are still relevent to somebody, feel free to
 restore them in -debug or any non-default mode of your choice.
---
 tactics/tactics.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fe3854143c..8546b03a17 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3897,10 +3897,10 @@ let unify ?(state=full_transparent_state) x y gl =
     in tclEVARS evd gl
   with e when Errors.noncritical e -> tclFAIL 0 (str"Not unifiable") gl
 
-let emit_side_effects eff gl = 
-  Declareops.iter_side_effects (fun e ->
+let emit_side_effects eff gl =
+(* Declareops.iter_side_effects (fun e ->
     prerr_endline ("emitting: " ^ Declareops.string_of_side_effect e))
-    eff;
+    eff; *)
   { it = [gl.it] ; sigma = Evd.emit_side_effects eff gl.sigma; }
 
 module Simple = struct
-- 
cgit v1.2.3