Fixing an inconsistency in interpreting Ltac names linking to binder names.

The recursion names in fix and cofix were not renamed like other
binders were.

2 files changed, 21 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.