From 9371ab87e8bac42216f882ed8f00e6fba9dc6eb0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Jun 2018 13:45:50 +0200
Subject: Fixing ltac names interpretation in internals of pattern-matching
 compilation.

The parts of pattern-matching compilation which generated names may
generate names which collided with names of the Ltac environment.

We fix it by avoiding the names of the Ltac environment.
---
 test-suite/success/ltac.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 3e19cfc8a6..4404ff3f16 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -358,3 +358,22 @@ Goal True.
 g 1.
 Abort.
 End ToMatchNames.
+
+(* An example where internal names used to build the return predicate
+   (here "n" because "a" is bound to "nil" and "n" is the first letter
+   of "nil") by small inversion should be taken distinct from Ltac names. *)
+
+Module LtacNames.
+Inductive t (A : Type) : nat -> Type :=
+    nil : t A 0 | cons : A -> forall n : nat, t A n -> t A (S n).
+
+Ltac f a n :=
+  let x := constr:(match a with nil _ => true | cons _ _ _ _ => I end) in
+  assert (x=x/\n=n).
+
+Goal forall (y:t nat 0), True.
+intros.
+f y true.
+Abort.
+
+End LtacNames.
-- 
cgit v1.2.3