From 8376231c9767d6f026ac9afc8e48c5d56cd803b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 18:06:23 +0200
Subject: Accept local variables in mixed terms and binders of notations.

---
 interp/constrintern.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c90d789105..032a752fe0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1645,6 +1645,8 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
   in
   let rec drop_syndef test_kind ?loc scopes qid pats =
     try
+      if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids then
+        raise Not_found;
       match Nametab.locate_extended qid with
       | SynDef sp ->
         let filter (vars,a) =
-- 
cgit v1.2.3