diff options
| author | Pierre-Marie Pédrot | 2018-11-03 19:31:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-03 19:31:05 +0100 |
| commit | 2e970d6c7876963a9845cae4153fe39cac81b587 (patch) | |
| tree | 43677d80223aec8f5e2a3be2df2704d9cb295736 /plugins | |
| parent | 10e2f279d97b15939e6bdc7658dee20e09b06653 (diff) | |
| parent | 9f9591fd0fad76af5f0fcfee5ec665a9e246b931 (diff) | |
Merge PR #8745: Fixes #3468: making tactic-in-term sensitive to interpretation scopes
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 |