From 4dab4fc5b2c20e9b7db88aec25a920b56ac83cb6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 14 Apr 2018 23:35:43 +0200
Subject: 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.
---
 test-suite/success/ltac.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3