From 180775636f5ec93e95df681951fafb321f8ebe67 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 26 Jan 2017 00:53:23 +0100
Subject: 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).
---
 interp/topconstr.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp')

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
 
-- 
cgit v1.2.3