* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
let debug = true;;
let debug_print s = if debug then prerr_endline (Lazy.force s);;
let t' = ProofEngineReduction.simpl context t in
let simpl_order = !compare_terms t t' in
if simpl_order = Gt then
- (prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t'));
- t')
+ (* prerr_endline ("reduce: "^(CicPp.ppterm t)^(CicPp.ppterm t')); *)
+ t'
else t
;;