From c2336868843bfe0c8e8a0b669641ca09814a45df Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 17 Apr 2018 15:51:16 +0200
Subject: 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.
---
 pretyping/pretyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

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