diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2013-11-25 11:41:27 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2013-11-25 16:22:40 +0100 |
| commit | 619b04a80ac6b17d54ac9227cba2d597cbda00a9 (patch) | |
| tree | effb0c14f18a3012b82e948140d51ea0a2181738 /grammar | |
| 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 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 128b13bda..d884a10cb 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -170,7 +170,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = | _ -> <:expr< fun ist gl x -> let (sigma,a_interp) = - Tacinterp.interp_genarg ist gl + Tacinterp.interp_genarg ist + (Tacmach.pf_env gl) (Tacmach.project gl) (Tacmach.pf_concl gl) gl.Evd.it (Genarg.in_gen $make_globwit loc globtyp$ x) in (sigma , out_gen $make_topwit loc globtyp$ a_interp)>> |