From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 21 Jul 2009 20:21:22 +0000 (+0000)
Subject: Debugging code removed.
X-Git-Tag: make_still_working~3641
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71d8526b03b2b7f415404074b4a0d51b71afb85a;p=helm.git

Debugging code removed.
---

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 684874ce6..a124b2838 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -222,8 +222,6 @@ let mk_projection leftno tyname consname consty (projname,_,_) i =
        HExtlib.mk_list underscore (argsno - i -1) in
      let branch = CicNotationPt.Pattern (consname,None,bvars), bvar in
      let projs,outtype = nth_prod [] i ty in
-prerr_endline ("outtype[" ^ string_of_int i ^ "]: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
-prerr_endline ("XXX[" ^ string_of_int i ^ "]: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] outtype);
      let rels =
       List.map
        (fun name -> mk_appl (mk_id name :: List.rev names @ [arg])) projs