diff options
| author | aspiwack | 2013-11-02 15:42:07 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:42:07 +0000 |
| commit | 77a9e54384c4db36d9dc3c14a8a10e4c266066f0 (patch) | |
| tree | 0f8e7064465279d73208db511e8db663d97aea50 | |
| parent | d66eefb692b0eb825de83782fad95bdcc0e44781 (diff) | |
Fix the log of debug auto.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17035 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/auto.ml | 8 |
1 files 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 *) |