diff options
| author | Pierre-Marie Pédrot | 2018-09-25 10:43:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-25 10:43:57 +0200 |
| commit | 7eb8a7eb8d23ffaf149f71a46fb1b089b90db7f8 (patch) | |
| tree | aa480ca16c64e5c1e04ac31dd9bc8066f44840c1 /plugins/ssr/ssrparser.ml4 | |
| parent | 4ae5a0e2dec60f753d21385b88991a9d1f0ec62d (diff) | |
| parent | 6b61b63bb8626827708024cbea1312a703a54124 (diff) | |
Merge PR #6343: [engine] Remove and deprecate `nf_enter` et al.
Diffstat (limited to 'plugins/ssr/ssrparser.ml4')
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 |