From 89ff5b72ef74d831fd44e19111357c2d27a73fc2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Nov 2003 18:53:31 +0000
Subject: Ajout entrees

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8359 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/macros.tex | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/doc/macros.tex b/doc/macros.tex
index 4c940d5226..6b3c2ed3b0 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -87,6 +87,8 @@
 \newcommand{\Index}{\textrm{\textsl{index}}}
 \newcommand{\abbrev}{\textrm{\textsl{abbreviation}}}
 \newcommand{\annotation}{\textrm{\textsl{annotation}}}
+\newcommand{\returntype}{\textrm{\textsl{return\_type}}}
+\newcommand{\caseitem}{\textrm{\textsl{case\_item}}}
 \newcommand{\atomictac}{\textrm{\textsl{atomic\_tactic}}}
 \newcommand{\binders}{\textrm{\textsl{bindings}}}
 \newcommand{\binder}{\textrm{\textsl{binding}}}
@@ -126,6 +128,7 @@
 \newcommand{\nestedpattern}{\textrm{\textsl{nested\_pattern}}}
 \newcommand{\num}{\textrm{\textsl{num}}}
 \newcommand{\params}{\textrm{\textsl{params}}}
+\newcommand{\binderlet}{\textrm{\textsl{binder\_let}}}
 \newcommand{\pattern}{\textrm{\textsl{pattern}}}
 \newcommand{\pat}{\textrm{\textsl{pat}}}
 \newcommand{\pgs}{\textrm{\textsl{pgms}}}
-- 
cgit v1.2.3