From b032b1dd4eab94d5bd43f6daf5ca5f9939ebc895 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Oct 2009 20:18:17 +0000 Subject: [PATCH] removed printing --- helm/software/components/ng_tactics/nAuto.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) 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 = -- 2.39.2