Prise en compte du let-in dans lookup_*_as_renamed

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

1 files changed, 14 insertions, 4 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 978532c07..352d1297a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -242,9 +242,15 @@ let computable p k =
 
 let lookup_name_as_renamed ctxt t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
-    | IsProd (name,t,c') ->
+    | IsProd (name,_,c') ->
+	(match concrete_name avoid env_names name c' with
+           | (Some id,avoid') -> 
+	       if id=s then (Some n) 
+	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
+	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
+    | IsLetIn (name,_,_,c') ->
 	(match concrete_name avoid env_names name c' with
-             (Some id,avoid') -> 
+           | (Some id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
 	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
@@ -256,8 +262,12 @@ let lookup_index_as_renamed t n =
   let rec lookup n d c = match kind_of_term c with
     | IsProd (name,_,c') ->
 	  (match concrete_name [] empty_names_context name c' with
-          (Some _,_) -> lookup n (d+1) c'
-        | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+               (Some _,_) -> lookup n (d+1) c'
+             | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+    | IsLetIn (name,_,_,c') ->
+	  (match concrete_name [] empty_names_context name c' with
+             | (Some _,_) -> lookup n (d+1) c'
+             | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
     | IsCast (c,_) -> lookup n d c
     | _ -> None
   in lookup n 1 t