aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-02-01 10:52:28 +0100
committerPierre-Marie Pédrot2017-02-01 10:54:53 +0100
commitc17c3faee20251cd5c7168246e9ffcd12d557f85 (patch)
tree02635866b73d7595fad009cc17535a6bbf06c2fc /interp
parentf86bfa39cddfb9c6411ed8624cee9a2b5c8d53bd (diff)
parent568b38e1d599f8bac5adf140f5a114f2871bc436 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'interp')
-rw-r--r--interp/topconstr.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index b455381ea3..407cec0842 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -92,8 +92,9 @@ let rec fold_local_binders g f n acc b = function
f n (fold_local_binders g f n' acc b l) t
| LocalRawDef ((_,na),t)::l ->
f n (fold_local_binders g f (name_fold g na n) acc b l) t
- | LocalPattern _::l ->
- assert false
+ | LocalPattern (_,pat,t)::l ->
+ let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
+ Option.fold_left (f n) acc t
| [] ->
f n acc b