diff options
| author | herbelin | 2006-07-05 17:34:59 +0000 |
|---|---|---|
| committer | herbelin | 2006-07-05 17:34:59 +0000 |
| commit | 1c0e94cccb4689252982aa652fcb6b5aa03f0bcf (patch) | |
| tree | 3df5b6b9e33b4cd2e4c4f2fd881067a53566fe31 | |
| parent | 63bad80b792bbe5de56fb3f6c242fab3327aa041 (diff) | |
Ajout taclevel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9019 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | 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 53bbd258c9..3fe782d905 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -161,6 +161,7 @@ \newcommand{\form}{\textrm{\textsl{form}}} \newcommand{\entry}{\textrm{\textsl{entry}}} \newcommand{\proditem}{\textrm{\textsl{production\_item}}} +\newcommand{\taclevel}{\textrm{\textsl{tactic\_level}}} \newcommand{\tacargtype}{\textrm{\textsl{tactic\_argument\_type}}} \newcommand{\scope}{\textrm{\textsl{scope}}} \newcommand{\optscope}{\textrm{\textsl{opt\_scope}}} |