removed printing

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index d8e92cbad4172b6b3064d3ac4f9867851a1283c0..fbb43cbb0298d3e5c40113b761256a3eeec2c029 100644 (file)
--- 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 =