diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-11 13:53:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-07-11 13:53:53 +0000 |
| commit | f551066ede9f3f7151777bfe2dc253b2f9d790c0 (patch) | |
| tree | 344cc32a0e868587f55b11a96238bd3055404140 /doc/common | |
| parent | f6dbc9cf31f6a716a3a61832beac07e76347dcdb (diff) | |
Documentation de lazymatch et des extensions de idtac et fail
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9038 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/common')
| -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 3fe782d90..418fe1436 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -202,6 +202,7 @@ \newcommand{\str}{\textrm{\textsl{string}}} \newcommand{\subsequentletter}{\textrm{\textsl{subsequent\_letter}}} \newcommand{\switch}{\textrm{\textsl{switch}}} +\newcommand{\messagetoken}{\textrm{\textsl{message\_token}}} \newcommand{\tac}{\textrm{\textsl{tactic}}} \newcommand{\terms}{\textrm{\textsl{terms}}} \newcommand{\term}{\textrm{\textsl{term}}} |