Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.

This module contains:
- the former ExtraEnv in pretyping
- a few functions to traverse binders in pretyping.ml and cases.ml
- the part of pretyping dealing with genarg interpretation

The dependency of pretyping in an interpretation of names as names of
variables of identifier is now hidden in GlobEnv (no more explicit
"lvar" management in pretyping.ml). Similarly for the interpretation
of names as terms and for the interpretation of tactics-in-terms.

We keep empty_lvar in Glob_ops for compatibility, even though it is a
bit isolated there.

1 files changed, 10 insertions, 0 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 0f22a1f0a0..3e19cfc8a6 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -348,3 +348,13 @@ symmetry in H.
 match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *)
 exact (eq_refl H0).
 Abort.
+
+(* Check that internal names used in "match" compilation to push "term
+   to match" on the environment are not interpreted as ltac variables *)
+
+Module ToMatchNames.
+Ltac g c := let r := constr:(match c return _ with a => 1 end) in idtac.
+Goal True.
+g 1.
+Abort.
+End ToMatchNames.