diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/ptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index c24baea805..dbaf419588 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -245,7 +245,7 @@ let correctness s p opttac = deb_mess (str"Pred.red_cci: Reduction..." ++ fnl ()); let oc = reduce_open_constr oc in deb_mess (str"AFTER REDUCTION:" ++ fnl ()); - deb_mess (Printer.prterm_env (Global.env()) (snd oc)); + deb_print (Printer.prterm_env (Global.env())) (snd oc); let tac = (tclTHEN (Extratactics.refine_tac oc) automatic) in let tac = match opttac with | None -> tac |