From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 19 Apr 2002 11:12:29 +0000 (+0000)
Subject: Debugging stuff removed.
X-Git-Tag: V_0_3_0_debian_8~138
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7d44fa19cb262a8180a9e48d210311bf0732dbb3

Debugging stuff removed.
---

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 9771b7d82..58aaa0438 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -246,10 +246,7 @@ let reduce =
        in
         if l = [] then t' else C.Appl (t'::l)
  in
-function t -> let res =
-prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
   reduceaux []
-t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
 ;;
 
 exception WrongShape;;