Debugging code removed.

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 684874ce62bbdc87e22d0c4213aaa4dd583290d2..a124b28388d3fa83d38ad6a6a8d444724d963215 100644 (file)
--- 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