diff options
| author | Arnaud Spiwack | 2014-09-05 09:08:58 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-05 18:26:00 +0200 |
| commit | 2fcc458af16bbebb9748cb4220237e74452059fc (patch) | |
| tree | 170d751cda948d6dbf564fe50e5e755828261e1d /tactics | |
| 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')
| -rw-r--r-- | tactics/evar_tactics.ml | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
2 files changed, 3 insertions, 0 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 478019b41e..ace595a7bd 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -47,6 +47,7 @@ let instantiate_tac n (ist,rawc) ido = let lvar = { Pretyping.ltac_constrs = constrvars; ltac_uconstrs = Names.Id.Map.empty; + ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; } in let sigma' = w_refine (evk,evi) (lvar ,rawc) sigma in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5b0002d7e5..7d606402b0 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) = |