From f410308f7b300135d97b16ae3fbf776d8012bc61 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 Dec 2002 11:57:35 +0000
Subject: Evaluation paresseuse de l'affichage du debug

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3435 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/ptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3