diff options
| author | Hugo Herbelin | 2017-01-26 00:53:23 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-01-26 00:57:02 +0100 |
| commit | 180775636f5ec93e95df681951fafb321f8ebe67 (patch) | |
| tree | adcec1b329ec49b23c3c964890bf19319bc42ffb | |
| parent | e7bb95f2ac0d151cfdccea7b769413b332489cd3 (diff) | |
Fixing #5326 (anomaly on some unsupported case of 'pat).
We complete the support of 'pat in this particular case (a 'pat under
a binder in a notation).
| -rw-r--r-- | interp/topconstr.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 79eeacf354..d388376bc2 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 |