From 7d44fa19cb262a8180a9e48d210311bf0732dbb3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Apr 2002 11:12:29 +0000 Subject: [PATCH] Debugging stuff removed. --- helm/gTopLevel/proofEngineReduction.ml | 3 --- 1 file changed, 3 deletions(-) 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;; -- 2.39.2