diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:48:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:48:09 +0200 |
| commit | 91274486fab8712cb6b1c338704884c102ab005a (patch) | |
| tree | 634909e7388d466813a530a18441fafcb80f422d /checker/reduction.ml | |
| parent | 7a01de25661456406cc2d4a0edcef81af643889c (diff) | |
Remove debug printing code
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 19 |
1 files changed, 1 insertions, 18 deletions
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 |