diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 6 | ||||
| -rw-r--r-- | plugins/ssr/ssrfwd.mli | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 6d0b6de40d..757a7968ca 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -394,7 +394,7 @@ let rec pretty_rename evar_map term = function ppdebug(lazy Pp.(str"under: cannot pretty-rename all bound variables with destLambda")); term -let overtac gl = ssr_n_tac "over" ~-1 gl +let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1) let check_numgoals ?(minus = 0) nh = Proofview.numgoals >>= fun ng -> @@ -441,9 +441,9 @@ let undertac ist varnames ((dir,mult),_ as rule) hint = let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in check_numgoals ~minus:1 nh <*> Proofview.tclDISPATCH - ((List.map (function None -> Proofview.V82.tactic overtac + ((List.map (function None -> overtac | Some e -> ssrevaltac ist e <*> - Proofview.V82.tactic overtac) + overtac) (if hint = nullhint then [None] else snd hint)) @ [betaiota]) in diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index d57884c3ec..745560da03 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -63,4 +63,4 @@ val undertac : Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic val overtac : - Tacmach.tactic + unit Proofview.tactic |