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, 2 insertions, 2 deletions

diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 142b54513..a6aa08657 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -123,11 +123,11 @@ val check_evars_are_solved :
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
-  bool -> type_constraint -> env -> evar_map ref ->
+  int -> bool -> type_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_judgment
 
 val pretype_type :
-  bool -> val_constraint -> env -> evar_map ref ->
+  int -> bool -> val_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_type_judgment
 
 val ise_pretype_gen :