diff options
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 |