From 26a456cbf1e8abc5c033090b59892b314d7e7142 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 25 Sep 2020 21:41:48 +0200
Subject: Fixing printing part of #13078 (anomaly with binding notations in
 patterns).

We prevent notations involving binders (i.e. names or patterns) to be
used for printing in "match" patterns. The computation is done in
"has_no_binders_type", controlling uninterpretation.
---
 interp/notation_ops.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 354809252e..3ea3f3ccff 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1436,9 +1436,8 @@ let reorder_canonically_substitution terms termlists metas =
   List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
     match typ with
       | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
-      | NtnTypeBinder _ -> assert false
       | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
-      | NtnTypeBinderList -> assert false)
+      | NtnTypeBinder _ | NtnTypeBinderList -> anomaly (str "Unexpected binder in pattern notation."))
     metas ([],[])
 
 let match_notation_constr_cases_pattern c (metas,pat) =
-- 
cgit v1.2.3