From 71d8526b03b2b7f415404074b4a0d51b71afb85a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 Jul 2009 20:21:22 +0000 Subject: [PATCH] Debugging code removed. --- helm/software/components/ng_tactics/nCicElim.ml | 2 -- 1 file changed, 2 deletions(-) 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 -- 2.39.2