diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-05 09:08:58 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-05 18:26:00 +0200 |
| commit | 2fcc458af16bbebb9748cb4220237e74452059fc (patch) | |
| tree | 170d751cda948d6dbf564fe50e5e755828261e1d /tactics/tacinterp.ml | |
| parent | 8a1f5056e144c12e5e67aa7ac328cd65e730ede2 (diff) | |
Adds an identifier context in pretying's Ltac context.
Binder names are interpreted as the Ltac specified one if available.
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5b0002d7e..7d606402b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -492,6 +492,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = let vars = { Pretyping.ltac_constrs = constrvars; Pretyping.ltac_uconstrs = Id.Map.empty; + Pretyping.ltac_idents = Id.Map.empty; Pretyping.ltac_genargs = ist.lfun; } in let c = match ce with @@ -1313,6 +1314,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = let vars = { Pretyping.ltac_constrs = closure.typed; Pretyping.ltac_uconstrs = closure.untyped; + Pretyping.ltac_idents = Id.Map.empty; Pretyping.ltac_genargs = ist.lfun; } in let (sigma,c_interp) = |