diff options
| author |  Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
| commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
| tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /pretyping/matching.ml | |
| parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) | |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'pretyping/matching.ml')
| -rw-r--r-- | pretyping/matching.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 89ca95cb..d99b8c9f 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -178,12 +178,15 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | PApp (PApp (h, a1), a2), _ -> sorec stk subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> let p = Array.length args2 - Array.length args1 in if p>=0 then let args21, args22 = array_chop p args2 in let c = mkApp(c2,args21) in - let subst = merge_binding allow_bound_rels stk n c subst in + let subst = + match meta with + | None -> subst + | Some n -> merge_binding allow_bound_rels stk n c subst in array_fold_left2 (sorec stk) subst args1 args22 else raise PatternMatchingFailure |