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/ssr | |
| 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/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 1f3c758e5c..f2f236f448 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1088,7 +1088,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;; (** Basic tactics *) -let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl -> +let rec fst_prod red tac = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in match EConstr.kind (Proofview.Goal.sigma gl) concl with | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 8b9c94f2db..a7aae5bd31 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1949,7 +1949,7 @@ ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg END let vmexacttac pf = - Goal.nf_enter begin fun gl -> + Goal.enter begin fun gl -> exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl)) end |