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 /stm | |
| 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 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 635bf9bf31..b7ba163309 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2009,7 +2009,7 @@ end = struct (* {{{ *) 1 goals in TaskQueue.join queue; let assign_tac : unit Proofview.tactic = - Proofview.(Goal.nf_enter begin fun g -> + Proofview.(Goal.enter begin fun g -> let gid = Goal.goal g in let f = try List.assoc gid res @@ -2301,7 +2301,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `Leaks -> Exninfo.iraise exn | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin let tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> if CList.mem_f Evar.equal (Proofview.Goal.goal gl) goals_to_admit then Proofview.give_up else Proofview.tclUNIT () |