diff options
author | 2017-05-25 16:06:47 +0200 | |
---|---|---|
committer | 2017-05-25 16:06:47 +0200 | |
commit | 4ad6dbef69f9fd4cb1b55efc252d67325068e6b1 (patch) | |
tree | 0c2c1f2310cf5751a2f97f29a0bfd5a8295d1da2 /plugins/ltac/tacinterp.ml | |
parent | 48d56f49b1db47f393ef3e0f31d1b22adf497afa (diff) | |
parent | 5c5f7c8d6a6ed8cbb99b12dde09fdbcc30ca8ab9 (diff) |
Merge PR#637: Short cleaning of the interpretation path for constr_with_bindings
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
-rw-r--r-- | plugins/ltac/tacinterp.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 8ed65c5d9..a9ec779d1 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)) @@ -2044,6 +2044,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 } @@ -2066,6 +2071,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'; () |