From c1359f0ec2a77210ec80ad44753817418f102270 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 23 Nov 2017 18:50:20 +0100
Subject: Extended documentation for notations referring to binders.

Talking about the difference between ident and pattern. Giving
examples.
---
 doc/common/macros.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 81def1674..6a28c5b3d 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}}
-- 
cgit v1.2.3