diff options
| author | Matthieu Sozeau | 2014-06-17 14:21:51 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-17 15:42:14 +0200 |
| commit | 2b7bede68c213fbb884c773c073ba31a886f41f4 (patch) | |
| tree | bb91ed3f2d7bf0dea38551cd5f7674842398b92d /kernel | |
| parent | d104b50b9c9a589d9fd8e44bdf56794c8aea4e53 (diff) | |
Fix a de Bruijn bug in checking code of projections.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index d6df6366cb..ec9541189a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -138,7 +138,7 @@ let check_projection env kn inst body = not (isLambda p) then cannot_recognize () in - let (na, t, ty) = destLambda p in + let (na, t, ty) = destLambda (Vars.subst1 mkProp p) in let argctx, p = decompose_lam_assum b.(0) in (* No need to check the lambdas as the case is well-formed *) let () = if not (isRel p) then cannot_recognize () in |