From 50d4df2da89461f280c302d032422856f8e77991 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 29 Feb 2008 19:24:57 +0000
Subject: Petite modif pour pouvoir faire "intros until 0" qui introduit autant
 que possible des variables qui ont déjà un nom joli tout plein. La
 conséquence c'est qu'on peut aussi faire "destruct 0" qui est vachement moins
 intéressant... Mais bon.

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

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b6ec169254..34e6945584 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -192,11 +192,24 @@ let lookup_index_as_renamed env t n =
     | Prod (name,_,c') ->
 	  (match concrete_name (Some true) [] empty_names_context name c' with
                (Name _,_) -> lookup n (d+1) c'
-             | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+             | (Anonymous,_) -> 
+		 if n=0 then
+		   Some (d-1)
+		 else if n=1 then 
+		   Some d 
+		 else 
+		   lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
 	  (match concrete_name (Some true) [] empty_names_context name c' with
              | (Name _,_) -> lookup n (d+1) c'
-             | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+             | (Anonymous,_) -> 
+		 if n=0 then 
+		   Some (d-1) 
+		 else if n=1 then 
+		   Some d 
+		 else 
+		   lookup (n-1) (d+1) c'
+	  )
     | Cast (c,_,_) -> lookup n d c
     | _ -> None
   in lookup n 1 t
-- 
cgit v1.2.3