Debugging stuff removed.

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 9771b7d821d023e861144e34b71234739d9feb8f..58aaa04386329ef8e0de0283fa449e84bc0612d2 100644 (file)
--- 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;;