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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2fc7843eda..31c0d20f32 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -383,7 +383,7 @@ open Decl_kinds prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level n | SetItemLevelAsBinder (l,bk,n) -> prlist_with_sep sep_v2 str l ++ - spc() ++ pr_at_level n ++ spc() ++ pr_constr_as_binder_kind bk + spc() ++ pr_at_level_opt n ++ spc() ++ pr_constr_as_binder_kind bk | SetLevel n -> pr_at_level (NumLevel n) | SetAssoc LeftA -> keyword "left associativity" | SetAssoc RightA -> keyword "right associativity" |