From 91274486fab8712cb6b1c338704884c102ab005a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 6 Sep 2014 11:48:09 +0200 Subject: Remove debug printing code --- checker/reduction.ml | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) (limited to 'checker/reduction.ml') diff --git a/checker/reduction.ml b/checker/reduction.ml index 0886ab748..aa9639e55 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -239,11 +239,6 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* compute the lifts that apply to the head of the term (hd1 and hd2) *) let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in - let () = Print.print_pure_constr (whd_val infos hd1); - Pp.pp (Pp.str " conv "); - Print.print_pure_constr (whd_val infos hd2); - Pp.ppnl (Pp.str "") - in match (fterm_of hd1, fterm_of hd2) with (* case of leaves *) | (FAtom a1, FAtom a2) -> @@ -442,19 +437,7 @@ let clos_fconv cv_pb env t1 t2 = let fconv cv_pb env t1 t2 = if eq_constr t1 t2 then () - else - try clos_fconv cv_pb env t1 t2 - with NotConvertible -> - let open Pp in - if !Flags.debug then ( - Pp.ppnl (str " conversion failed on: "); - Print.print_pure_constr t1; - Pp.ppnl (str " and "); - Print.print_pure_constr t2); - raise NotConvertible - - - + else clos_fconv cv_pb env t1 t2 let conv = fconv CONV let conv_leq = fconv CUMUL -- cgit v1.2.3