COQBIN plus necessaire, typos

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8417 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 38 insertions, 32 deletions

diff --git a/doc/Makefile b/doc/Makefile
index d1565888eb..424a3d1be7 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -1,6 +1,7 @@
 # Makefile for the Coq documentation
 
-# You need the environment variable COQBIN to be correctly set
+# if coqc,coqtop,coq-tex are not in your PATH, you need the environment 
+# variable COQBIN to be correctly set  
 # (COQTOP is autodetected)
 # (some files are preprocessed using Coq and some part of the documentation
 # is automatically built from the theories sources)
@@ -14,10 +15,17 @@
 #   - htmlSplit: http://coq.inria.fr/~delahaye
 # Rapports INRIA: dviselect, rrkit (par Michel Mauny)
 
-DOCCOQTOP=$(COQBIN)/coqtop #.byte
-DOCCOQC=$(COQBIN)/coqc
+
+ifeq ("$(COQBIN)","")
+ COQBINPATH =  
+else    
+ COQBINPATH = $(COQBIN)/
+endif
+
+DOCCOQTOP=$(COQBINPATH)coqtop #.byte
+DOCCOQC=$(COQBINPATH)coqc
 COQTOP=`$(DOCCOQC) -where`
-COQTEX=$(COQBIN)/coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small
+COQTEX=$(COQBINPATH)coq-tex -n 72 -image $(DOCCOQTOP) -v -sl -small
 #COQWEBSTY=$(HOME)/lib/tex/
 COQWEBSTY=/usr/share/texmf/tex/latex/misc/
 HEVEALIB=/usr/local/lib/hevea
@@ -76,8 +84,12 @@ FTPHTMLDOCS=doc-html.tar.gz
 all: check-env all-ps all-pdf
 
 check-env:
-	@if $(TEST) "$(COQBIN)" = ""; then echo "COQBIN undefined"; exit 1; fi
-	@if $(TEST) "$(COQTOP)" = ""; then echo "COQTOP undefined"; exit 1; fi
+	@if $(TEST) "$(COQBIN)" = ""; then \
+		if coq-tex; then true ; \
+		else echo "coq-tex not found, COQBIN undefined"; exit 1; fi; \
+	fi
+	@if $(TEST) "$(COQTOP)" = ""; then echo "COQTOP undefined"; exit 1; \
+		else echo "COQTOP = $(COQTOP)"; fi
 
 coq-part: $(REFMANCOQTEXFILES) $(COQTEXFILES) demos-programs library/libdoc.tex
 
@@ -245,7 +257,7 @@ library.coqweb.tex: library.files
 	cd $(COQTOP)/theories; \
 	coqweb --noweb -o $$WHERE/$@ --no-preamble `cat $$WHERE/library.files`
 
-GALLINA=$(COQBIN)/gallina
+GALLINA=$(COQBINPATH)gallina
 
 # On garde la liste de tous les *.v avec dates dans library.files.ls
 # Si elle a change depuis la derniere fois ou library.files n'existe pas
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 757a0e2ce5..b147fd659e 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -974,10 +974,8 @@ intros; split_Rmult.
 \end{coq_example}
 
 All this tactics has been written with the tactic language Ltac
-described in chapter~\ref{TacticLanguage}.\\
-
-More details are available in this document: {\tt
-http://coq.inria.fr/$\sim$desmettr/Reals.ps}.\\
+described in chapter~\ref{TacticLanguage}.  More details are available
+in document \url{http://coq.inria.fr/~desmettr/Reals.ps}.
 
 \begin{coq_eval}
 Reset Initial.
@@ -995,26 +993,21 @@ can be accessed by requiring module {\tt List}.
 \index{Contributions}
 \label{Contributions}
 
-Numerous users' contributions have been collected and are available on
-the WWW at the following address: \verb!coq.inria.fr/contribs/!.
-On this web page, you have a list of all contributions with
-informations (author, institution, quick description, etc.) and the
-possibility to download them one by one.
-There is a small search engine to look for keywords in all contributions.
-You will also find informations on how to submit a new contribution. 
+Numerous users' contributions have been collected and are available at
+URL \url{coq.inria.fr/contribs/}.  On this web page, you have a list
+of all contributions with informations (author, institution, quick
+description, etc.) and the possibility to download them one by one.
+There is a small search engine to look for keywords in all
+contributions.  You will also find informations on how to submit a new
+contribution.
 
 The users' contributions may also be obtained by anonymous FTP from site
 \verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and
-searchable on-line at 
-
-\begin{quotation}
-  \texttt{http://coq.inria.fr/contribs-eng.html}
-\end{quotation}
+searchable on-line at \url{http://coq.inria.fr/contribs-eng.html}
 
 % $Id$ 
 
-
 %%% Local Variables: 
 %%% mode: latex
-%%% TeX-master: t
+%%% TeX-master: "Reference-Manual"
 %%% End: 
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 78ba6cc92b..d5604ecc44 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -125,10 +125,10 @@ necessarily parsed surrounded by parentheses.
 notation & precedence/associativity \\
 \hline
 \verb$"_ , _"$ & 250 \\
-\verb$exists _ : _ | _$ & 200 \\
-\verb$exists _ | _$ & 200 \\
-\verb$exists2 _ : _ | _ & _$ & 200 \\
-\verb$exists2 _ | _ & _$ & 200 \\
+\verb$exists _ : _, _$ & 200 \\
+\verb$exists _, _$ & 200 \\
+\verb$exists2 _ : _, _ & _$ & 200 \\
+\verb$exists2 _, _ & _$ & 200 \\
 \verb$"_ <-> _"$ & 95 \\
 \verb$"_ -> _"$ & 90\, R (primitive) \\
 \verb$"_ \/ _"$ & 85\, R \\
@@ -153,7 +153,7 @@ notation & precedence/associativity \\
 \verb$"_ / _"$  & 40\, L \\
 \verb$"- _"$  & 35\, R \\
 \verb$"/ _"$  & 35\, R \\
-\verb$"_ ^ _"$  & 30\, L \\
+\verb$"_ ^ _"$  & 30\, R \\
 \verb$"{ _ } + { _ }"$ & 0 \\
 \verb$"_ + { _ }"$  & 50\, L \\
 \verb$"{ _ : _ | _ }"$ & 0 \\
@@ -389,7 +389,7 @@ notation are replaced by ``\_''.
 
 \begin{coq_example}
 Locate "exists".
-Locate "'exists' _ | _".
+Locate "'exists' _ , _".
 \end{coq_example}
 
 \SeeAlso Section \ref{Locate}.
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 92fbc42d84..af1ed0f29f 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -2140,7 +2140,8 @@ Variable g:A->A->A.
 \end{coq_eval}
 
 \begin{coq_example}
-Theorem T: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
+Theorem T: 
+  a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
 intros.
 congruence.
 \end{coq_example}