diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-23 13:30:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
| commit | 0c4eea2553d5b3b70d0b5baaf92781a544de83bd (patch) | |
| tree | c39bf3bff29cd7b8bb68b503ce53df7e6f382215 /vernac/metasyntax.ml | |
| parent | dcfd5c2c2cefcd8ae6a5b2e90fcbd98da4f1b120 (diff) | |
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.
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |