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.

3 files changed, 22 insertions, 1 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2d200ad27e..57a259b311 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -560,7 +560,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
       | None -> ()
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-    let _,newenv = push_rec_types !evdref (names,ftys) env in
+    let names,newenv = push_rec_types !evdref (names,ftys) env in
     let vdefj =
       Array.map2_i
 	(fun i ctxt def ->
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.