From 5b68ddd7b9a7a1596c14b78f06c980af5cd6a28d Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 9 Mar 2004 13:29:28 +0000
Subject: bug affichage des cofix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5442 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/detyping.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8bd6a1a018..d8c97bddd4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -374,9 +374,9 @@ and detype_cofix tenv avoid env n (names,tys,bodies) =
 	 let id = next_name_away na avoid in 
 	 (id::avoid, add_name (Name id) env, id::l))
       (avoid, env, []) names in
-  let n = Array.length tys in
+  let ntys = Array.length tys in
   let v = array_map2
-    (fun c t -> share_names tenv 0 [] def_avoid def_env c (lift n t))
+    (fun c t -> share_names tenv 0 [] def_avoid def_env c (lift ntys t))
     bodies tys in
   RRec(dummy_loc,RCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
-- 
cgit v1.2.3