diff options
| author | Emilio Jesus Gallego Arias | 2018-09-06 20:26:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-24 14:45:25 +0200 |
| commit | 6b61b63bb8626827708024cbea1312a703a54124 (patch) | |
| tree | ea4ed27e91ab36869a6dd262d29d52f497d77a96 /plugins/ltac/tactic_debug.ml | |
| parent | 1946a98e9f6e8cf9a619f01c406d9fc37dd56641 (diff) | |
[engine] Remove and deprecate `nf_enter` et al.
After the introduction of `EConstr`, "normalization" has become
unnecessary, we thus deprecate the `nf_*` family of functions.
Test-suite and CI pass after the fix for #8513.
Diffstat (limited to 'plugins/ltac/tactic_debug.ml')
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 105b5c59ae..48d677a864 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -58,7 +58,7 @@ let db_pr_goal gl = str" " ++ pc) ++ fnl () let db_pr_goal = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg)) end |