diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-19 18:26:40 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-19 18:26:40 +0000 |
| commit | dfab4556ba6a111a5bcbcb387ce2fdf546f9edf1 (patch) | |
| tree | c5077b4144f77e452045a2c051ed2e4cf06bbb7c /interp | |
| parent | d497b0068ba7262f98c13d53cc2e6a0f1d357b10 (diff) | |
Bug protection array_fold_left2
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5536 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/topconstr.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index f0011af06..1836524f3 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -371,7 +371,8 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with let sigma = List.fold_left2 (fun s (tm1,_) (tm2,_) -> match_ alp metas s tm1 tm2) sigma tml1 tml2 in List.fold_left2 (match_equations alp metas) sigma eqnl1 eqnl2 - | ROrderedCase (_,st,po1,c1,bl1,_), AOrderedCase (st2,po2,c2,bl2) -> + | ROrderedCase (_,st,po1,c1,bl1,_), AOrderedCase (st2,po2,c2,bl2) + when Array.length bl1 = Array.length bl2 -> let sigma = option_fold_left2 (match_ alp metas) sigma po1 po2 in array_fold_left2 (match_ alp metas) (match_ alp metas sigma c1 c2) bl1 bl2 | RCast(_,c1,t1), ACast(c2,t2) -> |