diff options
| author | aspiwack | 2008-02-29 19:24:57 +0000 |
|---|---|---|
| committer | aspiwack | 2008-02-29 19:24:57 +0000 |
| commit | 50d4df2da89461f280c302d032422856f8e77991 (patch) | |
| tree | 01e93ea00fd08ae5d46add22d72679cd28e0aff4 | |
| parent | 855cc609d2888ef59d848ed688f02390811b28c7 (diff) | |
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
| -rw-r--r-- | pretyping/detyping.ml | 17 |
1 files 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 |