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
;;