diff options
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 294cba4d7..e6d0370f3 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -12,7 +12,6 @@ open Pp open Tacexpr open Termops open Nameops -open Proofview.Notations let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () @@ -57,10 +56,10 @@ let db_pr_goal gl = str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_enter begin fun gl -> let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) - end } + end (* Prints the commands *) |