Merge PR #7288: Isolating ltac naming out of pretyping + fixing renaming

3 files changed, 50 insertions, 0 deletions

diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index eb9f571022..efdc94fb1e 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -38,3 +38,14 @@ Ltac foo :=
   let w := () in
   let z := 1 in
   pose v
+2 subgoals
+  
+  n : nat
+  ============================
+  (fix a (n0 : nat) : nat := match n0 with
+                             | 0 => 0
+                             | S n1 => a n1
+                             end) n = n
+
+subgoal 2 is:
+ forall a : nat, a = 0
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 901b1e3aa6..40e743c3f0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -71,3 +71,13 @@ Ltac foo :=
   let z := 1 in
   pose v.
 Print Ltac foo.
+
+(* Ltac renaming was not applied to "fix" and "cofix" *)
+
+Goal forall a, a = 0.
+match goal with
+|- (forall x, x = _) => assert (forall n, (fix x n := match n with O => O | S n => x n end) n = n)
+end.
+intro.
+Show.
+Abort.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 0f22a1f0a0..4404ff3f16 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -348,3 +348,32 @@ 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.
+
+(* 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.