diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 3 | ||||
| -rw-r--r-- | src/tac2intern.ml | 3 | ||||
| -rw-r--r-- | src/tac2intern.mli | 4 |
3 files changed, 10 insertions, 0 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 1f500352cf..81388af0ef 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -873,6 +873,9 @@ let () = let () = let intern ist tac = + (** Prevent inner calls to Ltac2 values *) + let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in + let ist = { ist with Genintern.extra } in let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in tac in diff --git a/src/tac2intern.ml b/src/tac2intern.ml index b9e77f3cf5..490436422d 100644 --- a/src/tac2intern.ml +++ b/src/tac2intern.ml @@ -169,6 +169,9 @@ let env_name env = let ltac2_env : environment Genintern.Store.field = Genintern.Store.field () +let drop_ltac2_env store = + Genintern.Store.remove store ltac2_env + let fresh_id env = UF.fresh env.env_cst let get_alias (loc, id) env = diff --git a/src/tac2intern.mli b/src/tac2intern.mli index 8c997b741e..95199d449d 100644 --- a/src/tac2intern.mli +++ b/src/tac2intern.mli @@ -43,3 +43,7 @@ val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr val error_nargs_mismatch : Loc.t -> ltac_constructor -> int -> int -> 'a val error_nparams_mismatch : Loc.t -> int -> int -> 'a + +(** Misc *) + +val drop_ltac2_env : Genintern.Store.t -> Genintern.Store.t |