aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/macros.tex
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-23 20:13:07 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-23 20:13:07 +0000
commit0c19d3acea1f5b9390a7cbb7c4b86cc8d976fdb4 (patch)
treede85c451b6200e54c564703737ec66a15b4cc568 /doc/macros.tex
parentcc0266d50f6a25dece037bff90d3b02498760ab3 (diff)
Ajout/renommage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8363 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/macros.tex')
-rwxr-xr-xdoc/macros.tex3
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/macros.tex b/doc/macros.tex
index 6b3c2ed3b..2bcffd354 100755
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -112,7 +112,8 @@
\newcommand{\fixpoint}{\textrm{\textsl{fixpoint}}}
\newcommand{\flag}{\textrm{\textsl{flag}}}
\newcommand{\form}{\textrm{\textsl{form}}}
-\newcommand{\gensymbol}{\textrm{\textsl{symbol}}}
+\newcommand{\entry}{\textrm{\textsl{entry}}}
+\newcommand{\symbolentry}{\textrm{\textsl{symbol}}}
\newcommand{\localassums}{\textrm{\textsl{local\_assums}}}
\newcommand{\localdef}{\textrm{\textsl{local\_def}}}
\newcommand{\localdecls}{\textrm{\textsl{local\_decls}}}