diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 37e4b625f0..6d3c5d8807 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -30,10 +30,12 @@ let get_index = function Locus.ArgArg i -> i | _ -> (** The "first" and "last" tacticals. *) -let tclPERM perm tac gls = - let subgls = tac gls in +let tclPERM perm tac = + Proofview.V82.tactic begin fun gls -> + let subgls = Proofview.V82.of_tactic tac gls in let subgll' = perm subgls.Evd.it in re_sig subgll' subgls.Evd.sigma + end let rot_hyps dir i hyps = let n = List.length hyps in @@ -45,20 +47,18 @@ let rot_hyps dir i hyps = rot (match dir with L2R -> i | R2L -> n - i) [] hyps let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) = - Proofview.V82.tactic begin let i = get_index ivar in - let evtac t = Proofview.V82.of_tactic (ssrevaltac ist t) in + let evtac t = ssrevaltac ist t in let tac1 = evtac atac1 in if atacs2 = [] && atac3 <> None then tclPERM (rot_hyps dir i) tac1 else - let evotac = function Some atac -> evtac atac | _ -> Tacticals.tclIDTAC in + let evotac = function Some atac -> evtac atac | _ -> Tacticals.New.tclIDTAC in let tac3 = evotac atac3 in let rec mk_pad n = if n > 0 then tac3 :: mk_pad (n - 1) else [] in match dir, mk_pad (i - 1), List.map evotac atacs2 with - | L2R, [], [tac2] when atac3 = None -> Tacticals.tclTHENFIRST tac1 tac2 - | L2R, [], [tac2] when atac3 = None -> Tacticals.tclTHENLAST tac1 tac2 - | L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 - | R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) - end + | L2R, [], [tac2] when atac3 = None -> Tacticals.New.tclTHENFIRST tac1 tac2 + | L2R, [], [tac2] when atac3 = None -> Tacticals.New.tclTHENLAST tac1 tac2 + | L2R, pad, tacs2 -> Tacticals.New.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 + | R2L, pad, tacs2 -> Tacticals.New.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) (** The "in" pseudo-tactical *)(* {{{ **********************************************) |