diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-17 15:15:34 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-17 15:15:34 +0000 |
| commit | 34d3b725ba27a9ec146d649da10f709d72e6ceff (patch) | |
| tree | 904fe94e7e650d789b67e4de7202ffa752437155 /pretyping/matching.ml | |
| parent | 8e4ba92321576e92dbe91b014287d3981447df98 (diff) | |
Correcting a bug in matching context on if.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8827 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/matching.ml')
| -rw-r--r-- | pretyping/matching.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 2b0a0ac7b..9f580b851 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -157,8 +157,8 @@ let matches_core convert allow_partial_app pat c = else raise PatternMatchingFailure | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> - let ctx,b2 = decompose_prod_n_assum ci.ci_cstr_nargs.(0) b2 in - let ctx',b2' = decompose_prod_n_assum ci.ci_cstr_nargs.(1) b2' in + 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 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 |