diff options
| author | Hugo Herbelin | 2018-10-16 10:25:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-31 18:22:41 +0100 |
| commit | 9f9591fd0fad76af5f0fcfee5ec665a9e246b931 (patch) | |
| tree | 3a9fca778a267bd3049b930d6984b037867dcba0 /plugins | |
| parent | ba110aab290cecc8847f3bc3b8396d5d1b9493b0 (diff) | |
Fixes rest of #3468 (tactic-in-term was not respecting scopes).
We do it by passing interning env to ltac interning.
Collecting scopes was already done by side-effect internally to
Constrintern. We expose the side-effect to ltac.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 5 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.mli | 1 |
2 files changed, 4 insertions, 2 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index fcbcfae115..5e2a9af7e5 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -44,6 +44,7 @@ type glob_sign = Genintern.glob_sign = { (* ltac variables and the subset of vars introduced by Intro/Let/... *) genv : Environ.env; extra : Genintern.Store.t; + intern_sign : Genintern.intern_variable_status; } let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ()) @@ -209,7 +210,7 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra; intern_sign} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { @@ -218,7 +219,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = ltac_extra = extra; } in let c' = - warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env Evd.(from_env env)) c + warn (Constrintern.intern_core scope ~pattern_mode ~ltacvars env Evd.(from_env env) intern_sign) c in (c',if !strict_check then None else Some c) diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index a9f2d76e30..178f6af71d 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -21,6 +21,7 @@ type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; genv : Environ.env; extra : Genintern.Store.t; + intern_sign : Genintern.intern_variable_status; } val make_empty_glob_sign : unit -> glob_sign |