diff options
| author | Pierre-Marie Pédrot | 2017-09-03 01:59:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-03 02:03:41 +0200 |
| commit | 4d5e3f3f00cb1848861b938ba1a57c33800d71a6 (patch) | |
| tree | 227b93bad3660ec16b4b0e2964e6bb2577d0d6b2 /src | |
| parent | f84c0b96f11d5d1f130d36c0c04597ddeca6001f (diff) | |
Fix coq/ltac2#16: Passing Ltac2 variables to Ltac1 via $ results in anomalies.
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 |