Bug nommage des fonctions définies par récursion mutuelle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2205 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 5 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 714b7f6821..b634b04435 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -257,11 +257,14 @@ let rec detype avoid env t =
     | CoFix (n,recdef) -> detype_fix avoid env (RCoFix n) recdef
 
 and detype_fix avoid env fixkind (names,tys,bodies) =
-  let lfi = Array.map (fun id -> next_name_away id avoid) names in
-  let def_avoid = Array.to_list lfi@avoid in
-  let def_env =
-    Array.fold_left (fun env id -> add_name (Name id) env) env lfi in
-  RRec(dummy_loc,fixkind,lfi,Array.map (detype avoid env) tys,
+  let def_avoid, def_env, lfi =
+    Array.fold_left
+      (fun (avoid, env, l) na ->
+	 let id = next_name_away na avoid in 
+	 (id::avoid, add_name (Name id) env, id::l))
+      (avoid, env, []) names in
+  RRec(dummy_loc,fixkind,Array.of_list (List.rev lfi),
+       Array.map (detype avoid env) tys,
        Array.map (detype def_avoid def_env) bodies)