diff options
Diffstat (limited to 'pretyping/matching.ml')
| -rw-r--r-- | pretyping/matching.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 9ce8e703f..ada3b912b 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -161,7 +161,8 @@ let matches_core convert allow_partial_app pat c = | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_nargs.(0) b2 in let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_nargs.(1) b2' in - let n = List.length ctx and n' = List.length ctx' in + let n = rel_context_length ctx in + let n' = rel_context_length ctx' in if noccur_between 1 n b2 & noccur_between 1 n' b2' then let s = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx in let s' = List.fold_left (fun l (na,_,t) -> (na,t)::l) stk ctx' in |