From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 24 Jul 2009 22:05:29 +0000 (+0000)
Subject: Debugging code removed.
X-Git-Tag: make_still_working~3620
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4a6973c769b96f569b4aa5410197e0e6c76dfc92;p=helm.git

Debugging code removed.
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index be069fce1..5c418ac9d 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -1020,7 +1020,6 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
                assert (metasenv = [] && subst = []);
                let ty = NCicTypeChecker.typeof ~subst ~metasenv [] t in
                let src,tgt = src_tgt_of_ty_cpos_arity ty cpos arity in
-prerr_endline ("COERCION " ^ name ^ " cpos = " ^ string_of_int cpos ^ " arity = " ^ string_of_int arity);
                 basic_eval_and_inject_ncoercion (name,t,src,tgt,cpos,arity)
                  status
              ) status coercions