diff options
author | 2014-09-17 16:20:50 +0200 | |
---|---|---|
committer | 2014-09-17 17:57:08 +0200 | |
commit | 17f68d403d248e899efbb76afeed169232946ecf (patch) | |
tree | 5eb60ef760ea388670612c4c0ece96a43e7dad87 /tactics/tacinterp.ml | |
parent | cc6afad3bcfaa5b7fa57c8cd3035fe520c93afda (diff) |
Fix bug #3633 properly, by delaying the interpetation of constrs in
apply f, g,... so that apply f, g. succeeds when apply f; apply g
does. It just mimicks the behavior of rewrite foo bar.
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r-- | tactics/tacinterp.ml | 21 |
1 files changed, 9 insertions, 12 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index abaee194e..ab2dbe6ff 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -899,16 +899,12 @@ let loc_of_bindings = function | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l)) | ExplicitBindings l -> pi1 (List.last l) -let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = +let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let loc1 = loc_of_glob_constr c in let loc2 = loc_of_bindings bl in let loc = if Loc.is_ghost loc2 then loc1 else Loc.merge loc1 loc2 in - let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in - sigma, (loc,cb) - -let interp_open_constr_with_bindings_arg_loc ist env sigma (keep,c) = - let sigma, c = interp_open_constr_with_bindings_loc ist env sigma c in - sigma,(keep,c) + let f env sigma = interp_open_constr_with_bindings ist env sigma cb in + (loc,f) let interp_induction_arg ist gl arg = let env = pf_env gl and sigma = project gl in @@ -1704,14 +1700,15 @@ and interp_atomic ist tac : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in - let sigma, l = - List.fold_map (interp_open_constr_with_bindings_arg_loc ist env) sigma cb - in + let l = List.map (fun (k,c) -> + let loc, f = interp_open_constr_with_bindings_loc ist c in + (k,(loc,f))) cb + in let sigma,tac = match cl with - | None -> sigma, fun l -> Tactics.apply_with_bindings_gen a ev l + | None -> sigma, fun l -> Tactics.apply_with_delayed_bindings_gen a ev l | Some cl -> let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in - sigma, fun l -> Tactics.apply_in a ev clear id l cl in + sigma, fun l -> Tactics.apply_delayed_in a ev clear id l cl in Tacticals.New.tclWITHHOLES ev tac sigma l end | TacElim (ev,(keep,cb),cbo) -> |