From fb73dae49f461f5ec81af870ce8279d619ebef9a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Jun 2010 13:56:19 +0000
Subject: Added documentation: "Theorem id x1..xn : T" and "Set Automatic
 Introduction". Updated documentation in many ways: - merged binder and
 binderlet as done for a while in implementation - fixed a few technical
 problems (bad indexation of {x:A|P x}, missing   spaces in html code in many
 situations due to missing curly brackets   around TeX macros - e.g. around
 \ldots -, missing dots at end of   sentences, ...) - renamed "statement"
 commands into "assertion" commands and   "declaration" commands into
 "assumption" commands - moved Goal and Save out of the Gallina chapter -
 avoid some recovering in the Gallina and proof mode chapters - slight
 smoothing of some hard-to-read paragraphs of the manual

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13091 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/common/macros.tex | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index c4e7973636..f0fb0883bb 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -75,8 +75,8 @@
 \newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
 %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
 %\newcommand{\onemany}[1]{$\{$#1$\}$+}
-\newcommand{\nelist}[2]{{#1} {\tt #2} {\ldots} {\tt #2} {#1}}
-\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2} {\ldots} {\tt #2} {#1}{\sl ]}}
+\newcommand{\nelist}[2]{{#1} {\tt #2}~{\ldots}~{\tt #2} {#1}}
+\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2}~{\ldots}~{\tt #2} {#1}{\sl ]}}
 \newcommand{\nelistwithoutblank}[2]{#1{\tt #2}\ldots{\tt #2}#1}
 \newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\ldots{\tt #2}#1$]$}
 
@@ -123,8 +123,7 @@
 \newcommand{\assums}{\nterm{assums}} % vernac
 \newcommand{\simpleassums}{\nterm{simple\_assums}} % assumptions
 \newcommand{\binder}{\nterm{binder}}
-\newcommand{\binderlet}{\nterm{binderlet}}
-\newcommand{\binderlist}{\nterm{binderlist}}
+\newcommand{\binders}{\nterm{binders}}
 \newcommand{\caseitems}{\nterm{match\_items}}
 \newcommand{\caseitem}{\nterm{match\_item}}
 \newcommand{\eqn}{\nterm{equation}}
@@ -137,10 +136,11 @@
 \newcommand{\params}{\nterm{params}} % vernac
 \newcommand{\returntype}{\nterm{return\_type}}
 \newcommand{\idparams}{\nterm{ident\_with\_params}}
-\newcommand{\statkwd}{\nterm{statement\_keyword}} % vernac
+\newcommand{\statkwd}{\nterm{assertion\_keyword}} % vernac
 \newcommand{\termarg}{\nterm{arg}}
 
-\newcommand{\typecstr}{\zeroone{{\tt :} {\term}}}
+\newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}}
+\newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}}
 
 
 \newcommand{\Fwterm}{\nterm{Fwterm}}
@@ -154,8 +154,8 @@
 \newcommand{\commandtac}{\nterm{tactic\_invocation}}
 \newcommand{\constructor}{\nterm{constructor}}
 \newcommand{\convtactic}{\nterm{conv\_tactic}}
-\newcommand{\declarationkeyword}{\nterm{declaration\_keyword}}
-\newcommand{\declaration}{\nterm{declaration}}
+\newcommand{\assumptionkeyword}{\nterm{assumption\_keyword}}
+\newcommand{\assumption}{\nterm{assumption}}
 \newcommand{\definition}{\nterm{definition}}
 \newcommand{\digit}{\nterm{digit}}
 \newcommand{\exteqn}{\nterm{ext\_eqn}}
@@ -211,7 +211,7 @@
 \newcommand{\simplepattern}{\nterm{simple\_pattern}}
 \newcommand{\sort}{\nterm{sort}}
 \newcommand{\specif}{\nterm{specif}}
-\newcommand{\statement}{\nterm{statement}}
+\newcommand{\assertion}{\nterm{assertion}}
 \newcommand{\str}{\nterm{string}}
 \newcommand{\subsequentletter}{\nterm{subsequent\_letter}}
 \newcommand{\switch}{\nterm{switch}}
-- 
cgit v1.2.3