diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/coretactics.ml4 | 4 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 18 |
3 files changed, 15 insertions, 9 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 28ff6df838..2d1220385a 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -141,10 +141,10 @@ END (** Specialize *) TACTIC EXTEND specialize - [ "specialize" constr_with_bindings(c) ] -> [ + [ "specialize" open_constr_with_bindings(c) ] -> [ Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) ] -| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ +| [ "specialize" open_constr_with_bindings(c) "as" intropattern(ipat) ] -> [ Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) ] END diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index bd48614dbc..a3b3fae0b3 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -190,7 +190,7 @@ let onSomeWithHoles tac = function | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c)) TACTIC EXTEND contradiction - [ "contradiction" constr_with_bindings_opt(c) ] -> + [ "contradiction" open_constr_with_bindings_opt(c) ] -> [ onSomeWithHoles contradiction c ] END diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b8c021f188..051cd31b2b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -996,7 +996,7 @@ let interp_bindings ist env sigma = function let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in - let sigma, c = interp_open_constr ist env sigma c in + let sigma, c = interp_constr ist env sigma c in sigma, (c,bl) let interp_open_constr_with_bindings ist env sigma (c,bl) = @@ -1025,7 +1025,7 @@ let interp_destruction_arg ist gl arg = | keep,ElimOnConstr c -> keep,ElimOnConstr { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = interp_constr_with_bindings ist env sigma c in + let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in Sigma.Unsafe.of_pair (c, sigma) } | keep,ElimOnAnonHyp n as x -> x @@ -1678,8 +1678,8 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = project gl in - let sigma, cb = interp_constr_with_bindings ist env sigma cb in - let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in + let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in let named_tac = let tac = Tactics.elim ev keep cb cbo in name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac @@ -1690,7 +1690,7 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in - let sigma, cb = interp_constr_with_bindings ist env sigma cb in + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in let named_tac = let tac = Tactics.general_case_analysis ev keep cb in name_atomic ~env (TacCase(ev,(keep,cb))) tac @@ -1807,7 +1807,7 @@ and interp_atomic ist tac : unit Proofview.tactic = in let l,lp = List.split l in let sigma,el = - Option.fold_map (interp_constr_with_bindings ist env) sigma el in + Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in let tac = name_atomic ~env (TacInductionDestruct(isrec,ev,(lp,el))) (Tactics.induction_destruct isrec ev (l,el)) @@ -2045,6 +2045,11 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm Sigma.Unsafe.of_pair (c, sigma) } +let interp_open_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigma -> + let (sigma, c) = interp_open_constr_with_bindings ist env (Sigma.to_evar_map sigma) c in + Sigma.Unsafe.of_pair (c, sigma) + } + let interp_destruction_arg' ist c = Ftactic.enter { enter = begin fun gl -> Ftactic.return (interp_destruction_arg ist gl c) end } @@ -2067,6 +2072,7 @@ let () = register_interp0 wit_open_constr (lifts interp_open_constr); register_interp0 wit_bindings interp_bindings'; register_interp0 wit_constr_with_bindings interp_constr_with_bindings'; + register_interp0 wit_open_constr_with_bindings interp_open_constr_with_bindings'; register_interp0 wit_destruction_arg interp_destruction_arg'; () |