From 0c4eea2553d5b3b70d0b5baaf92781a544de83bd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 23 Nov 2017 13:30:36 +0100
Subject: Change default for notations with variables bound to both terms and
 binders.

For compatibility, the default is to parse as ident and not as pattern.
---
 vernac/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/metasyntax.ml')

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 524c9b32b..bcffe640c 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -831,7 +831,7 @@ let interp_modifiers modl = let open NotationMods in
         if Id.List.mem_assoc id acc.etyps then
           user_err ~hdr:"Metasyntax.interp_modifiers"
             (str s ++ str " is already assigned to an entry or constr level.");
-        let typ = ETConstrAsBinder (bk,Some n) in
+        let typ = ETConstrAsBinder (bk,n) in
         interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevelAsBinder (idl,bk,n)::l)
     | SetLevel n :: l ->
         interp { acc with level = Some n; } l
-- 
cgit v1.2.3