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

1 files changed, 9 insertions, 9 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index c4e797363..f0fb0883b 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}}