diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c9e68d1e3..f0203fa2c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -260,8 +260,8 @@ and contract_branch isgoal e (cn,mkpat,b) = let is_nondep_branch c n = try - let _,ccl = decompose_lam_n_assum n c in - noccur_between 1 n ccl + let sign,ccl = decompose_lam_n_assum n c in + noccur_between 1 (rel_context_length sign) ccl with _ -> (* Not eta-expanded or not reduced *) false |