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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index cca1b2989..d90fd3eb7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1174,7 +1174,8 @@ GEXTEND Gram | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) | x = IDENT; "at"; lev = level -> SetItemLevel ([x],lev) - | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,lev) + | x = IDENT; "at"; lev = level; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,Some lev) + | x = IDENT; b = constr_as_binder_kind -> SetItemLevelAsBinder ([x],b,None) | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ) ] ] ; |