From 77a9e54384c4db36d9dc3c14a8a10e4c266066f0 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:42:07 +0000
Subject: Fix the log of debug auto.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17035 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 29381c7c82..1205d97001 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1194,8 +1194,8 @@ let tclLOG (dbg,depth,trace) pp tac =
 	  raise reraise
       end
 
-(* arnaud: todo replug debug auto *)
-let new_tclLOG (dbg,depth,trace) pp tac = tac
+let new_tclLOG dbg pp tac =
+  Proofview.V82.tactic (tclLOG dbg pp (Proofview.V82.of_tactic tac))
 
 (** For info, from the linear trace information, we reconstitute the part
     of the proof tree we're interested in. The last executed tactic
@@ -1243,8 +1243,8 @@ let tclTRY_dbg d tac =
       if level == Info then msg_debug (pr_info_nop d);
       tclIDTAC gl)
 
-(* arnaud: todo: rebrancher debug auto *)
-let new_tclTRY_dbg tac = Tacticals.New.tclTRY
+let new_tclTRY_dbg d tac =
+  Proofview.V82.tactic (tclTRY_dbg d (Proofview.V82.of_tactic tac))
 
 (**************************************************************************)
 (*                           The Trivial tactic                           *)
-- 
cgit v1.2.3