diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-23 20:13:07 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-23 20:13:07 +0000 |
commit | 0c19d3acea1f5b9390a7cbb7c4b86cc8d976fdb4 (patch) | |
tree | de85c451b6200e54c564703737ec66a15b4cc568 /doc/macros.tex | |
parent | cc0266d50f6a25dece037bff90d3b02498760ab3 (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-x | doc/macros.tex | 3 |
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}}} |