diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-13 16:49:32 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-13 16:49:32 +0000 |
| commit | a56e9f43716aa10cf041c94edbf9b06fd54ae602 (patch) | |
| tree | a319d6a8b604720ddf4d0399fb7f4225b697c052 /doc/common | |
| parent | 82a5090ac5263f500aedae328c24551e11c80acf (diff) | |
Documentation of records defined with the keywords Inductive and
CoInductive.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15161 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 f0fb0883b..ce998a9bc 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -206,6 +206,7 @@ %END LATEX %HEVEA \renewcommand{\proof}{\nterm{proof}} \newcommand{\record}{\nterm{record}} +\newcommand{\recordkw}{\nterm{record\_keyword}} \newcommand{\rewrule}{\nterm{rewriting\_rule}} \newcommand{\sentence}{\nterm{sentence}} \newcommand{\simplepattern}{\nterm{simple\_pattern}} |