diff options
| author | Hugo Herbelin | 2017-11-23 13:30:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:07 +0100 |
| commit | 0c4eea2553d5b3b70d0b5baaf92781a544de83bd (patch) | |
| tree | c39bf3bff29cd7b8bb68b503ce53df7e6f382215 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 0b5009e26b..d16c9bb802 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -214,7 +214,7 @@ type proof_expr = type syntax_modifier = | SetItemLevel of string list * Extend.production_level - | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level + | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option | SetLevel of int | SetAssoc of Extend.gram_assoc | SetEntryType of string * Extend.simple_constr_prod_entry_key |