diff options
| author | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-06 17:18:59 +0200 |
| commit | e5581b2a1e5b3d9fc5dc7fe95ee4ba121f5d42cd (patch) | |
| tree | 1a0d0b7d693c37ca8712057e946587584687208e /plugins/ltac/tactic_debug.ml | |
| parent | 2f23c27e08f66402b8fba4745681becd402f4c5c (diff) | |
| parent | 0ce9cef0ac431e184c870617841bedc3f427396d (diff) | |
Merge PR#623: Remove the Sigma (monotonous state) API.
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 294cba4d75..e6d0370f36 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 *) |