Fixing #4221 (interpreting bound variables using ltac env was possibly

capturing bound names unexpectingly).

We moved renaming to after finding bindings, i.e. in pretyping
"fun x y => x + y" in an ltac environment where y is ltac-bound to x,
we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1"
(which later on is displayed into "fun y y0 => y + y0").

We renounced to renaming in "match" patterns, which was anyway not
working well, as e.g. in

let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0).

which was producing

forall z : nat, match z with 0 => z | S y => y end = 0

because the names in default branches are treated specifically.

It would be easy to support renaming in match again, by putting the
ltac env in the Cases.pattern_matching_problem state and to rename the
names in "typs" (from build_branch), just before returning them at the
end of the function (and similarly in abstract_predicate for the names
occurring in the return predicate).

However, we rename binders in fix which were not interpreted.

There are some difficulties with evar because we want them defined in
the interpreted env (see comment to ltac_interp_name_env).

fix ltac name

1 files changed, 8 insertions, 0 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index badce063e..952f35bc3 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -298,3 +298,11 @@ evar(foo:nat).
 let evval := eval compute in foo in not_eq evval 1.
 let evval := eval compute in foo in not_eq 1 evval.
 Abort.
+
+(* Check instantiation of binders using ltac names *)
+
+Goal True.
+let x := ipattern:y in assert (forall x y, x = y + 0).
+intro.
+destruct y. (* Check that the name is y here *).
+Abort.