diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ae7106fb3..177389c98 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1316,7 +1316,7 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t = (* d1 ... dn dn+1 ... dn'-p+1 ... dn' *) (* \--env-/ (= x:ty) *) (* \--------------extenv------------/ *) - let (p,_) = lookup_rel_id x (rel_context extenv) in + let (p,_,_) = lookup_rel_id x (rel_context extenv) in let rec aux n (_,b,ty) = match b with | Some c -> |