From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 7 Oct 2009 20:18:17 +0000 (+0000)
Subject: removed printing
X-Git-Tag: make_still_working~3353
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b032b1dd4eab94d5bd43f6daf5ca5f9939ebc895;p=helm.git

removed printing
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index d8e92cbad..fbb43cbb0 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1004,11 +1004,7 @@ let get_candidates status context gty =
     NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe gty
   in
   (* XXX we have to trie for the context *)
-  let cands = NDiscriminationTree.TermSet.elements cands in
-  List.iter (fun x -> 
-    debug_print (lazy (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context x)))
-    cands;
-  cands
+  NDiscriminationTree.TermSet.elements cands
 ;;
 
 let applicative_case signature status flags g gty cache context =