diff options
author | 2016-10-23 21:26:20 +0200 | |
---|---|---|
committer | 2017-05-22 12:06:59 +0200 | |
commit | 9eb2f7480de8ded94a1b96eb4f6cc16d19a8c14d (patch) | |
tree | 70115d49a0ca45c6fa06a5978878ccb7ae302987 /plugins/ltac/tacinterp.ml | |
parent | 11851daee3a14f784cc2a30536a8f69be62c4f62 (diff) |
Clarifying the interpretation path for the "constr_with_binding" argument.
This fixes an inconsistency introduced in 554a6c806 (svn r12603) where
both interp_constr_with_bindings and interp_open_constr_with_bindings
were going through interp_open_constr (no type classes so as to not to
commit too early on irreversible choices, accepting unresolved holes).
We fix this by having interp_constr_with_bindings going to
interp_constr (using type classes and failing on unresolved evars).
The external impact is that any TACTIC EXTEND which refers to
constr_with_binding has now to decide whether it intends it to use
what the name suggest (using type classes and to fail if evars remain
unresolved), thus keeping constr_with_binding, or the actual behavior
which requires to use open_constr_with_bindings for strict
compatibility.
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 b8c021f18..051cd31b2 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'; () |