diff options
| author | Arnaud Spiwack | 2013-11-25 11:41:27 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-11-25 16:22:40 +0100 |
| commit | 619b04a80ac6b17d54ac9227cba2d597cbda00a9 (patch) | |
| tree | effb0c14f18a3012b82e948140d51ea0a2181738 /tactics/extraargs.ml4 | |
| parent | 32c900252a07ea7d2dd9fe15feb21ef98aee3df7 (diff) | |
Tacinterp: fewer use of old-style goals.
There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics.
I've changed some of them to explicitely take an environment and an evar_map instead.
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 5dcbd73a80..ccc231cf2d 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -141,12 +141,12 @@ let intern_place ist = function ConclLocation () -> ConclLocation () | HypLocation (id,hl) -> HypLocation (Tacintern.intern_hyp ist id,hl) -let interp_place ist gl = function +let interp_place ist env = function ConclLocation () -> ConclLocation () - | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist gl id,hl) + | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist env id,hl) let interp_place ist gl p = - Tacmach.project gl , interp_place ist gl p + Tacmach.project gl , interp_place ist (Tacmach.pf_env gl) p let subst_place subst pl = pl |