diff options
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 |