diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ba2d2fdf39..8d8a9950e3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -211,7 +211,7 @@ let lookup_index_as_renamed env t n = lookup (n-1) (d+1) c' ) | Cast (c,_,_) -> lookup n d c - | _ -> None + | _ -> if n=0 then Some (d-1) else None in lookup n 1 t (**********************************************************************) |