diff options
| author | Erik Martin-Dorel | 2019-03-01 17:07:41 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:43 +0200 |
| commit | c02ac6657863ba08b4c5f52dddf770d864ee6d4c (patch) | |
| tree | 594083627f4eac352d4828962a8e0eea06584b66 /plugins | |
| parent | 01b5e6e64b2af828b18fa6ee7037a7b7055f026e (diff) | |
[ssr] over: Expose the new type of tactic for Ssrfwd.overtac
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 |