From e0eaf3a49b6fb5feed1d55ca5cb356d601f54267 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2003 21:16:05 +0000
Subject: Réinstallation d'un afficheur de niveau d'imbrication pour le
 déboggueur de tactique

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4125 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/first-order/ground.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4
index 78887715a0..926a7918a3 100644
--- a/contrib/first-order/ground.ml4
+++ b/contrib/first-order/ground.ml4
@@ -42,7 +42,7 @@ let _=
       
 let ground_tac solver startseq gl=
   let rec toptac seq gl=
-    if Tacinterp.get_debug()=Tactic_debug.DebugOn 
+    if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
     then Pp.msgnl (Proof_trees.pr_goal (sig_it gl));
     match seq.gl with 
 	Atomic t->
-- 
cgit v1.2.3