From 34ce92b048ee33d78f40b661da5e35db782bcce5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 20 Mar 2002 09:43:20 +0000
Subject: renversement du renommage des variables

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2552 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/ocaml.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'contrib')

diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 78221b1be8..5be62058c2 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -89,12 +89,18 @@ let rec rename_vars avoid = function
       let (idl', avoid') = rename_vars avoid idl in
       (id :: idl', avoid')
   | id :: idl ->
-      let id' = rename_id (lowercase_id id) avoid in
-      let (idl', avoid') = rename_vars (Idset.add id' avoid) idl in
-      (id' :: idl', avoid')
+      let (idl, avoid) = rename_vars avoid idl in
+      let id = rename_id (lowercase_id id) avoid in
+      (id :: idl, Idset.add id avoid)
 
 let rename_tvars avoid l = 
-  let l',_ = rename_vars avoid l in 
+  let rec rename avoid = function 
+    | [] -> [],avoid 
+    | id :: idl -> 
+	let id = rename_id (lowercase_id id) avoid in 
+	let idl, avoid = rename (Idset.add id avoid) idl in 
+	(id :: idl, avoid) in
+  let l',_ = rename avoid l in 
   l', List.fold_left2 (fun m i i' -> Idmap.add i i' m) Idmap.empty l l'
 
 let push_vars ids (db,avoid) =
-- 
cgit v1.2.3