diff options
| author | Hugo Herbelin | 2017-11-23 18:50:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:08 +0100 |
| commit | c1359f0ec2a77210ec80ad44753817418f102270 (patch) | |
| tree | 2ff6ec52524af8dd6bd0652b5b7e4d9e44565e18 /doc/common | |
| parent | 0af54860172efe1aa5da419b81e4cb34348320ee (diff) | |
Extended documentation for notations referring to binders.
Talking about the difference between ident and pattern. Giving
examples.
Diffstat (limited to 'doc/common')
| -rw-r--r-- | doc/common/macros.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 81def1674c..6a28c5b3d1 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -182,6 +182,7 @@ \newcommand{\declnotation}{\nterm{decl\_notation}} \newcommand{\symbolentry}{\nterm{symbol}} \newcommand{\modifiers}{\nterm{modifiers}} +\newcommand{\binderinterp}{\nterm{binder\_interp}} \newcommand{\localdef}{\nterm{local\_def}} \newcommand{\localdecls}{\nterm{local\_decls}} \newcommand{\ident}{\nterm{ident}} |