coqide menus on golas

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

6 files changed, 46 insertions, 10 deletions

diff --git a/doc/Makefile b/doc/Makefile
index a6f561093..d1565888e 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -280,8 +280,8 @@ demos-programs:
 
 Recursive-Definition.v.tex: ./title.tex Recursive-Definition.tex
 
-Tutorial.v.dvi: ./title.tex Tutorial.v.tex
-Tutorial.v.pdf: ./title.tex Tutorial.v.tex
+Tutorial.v.dvi: ./version.tex ./title.tex Tutorial.v.tex
+Tutorial.v.pdf: ./version.tex ./title.tex Tutorial.v.tex
 
 # RefMan-ppr.v.tex: ../tactics/eqdecide.cmo
 
diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 223585d54..87c8e3edb 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -160,7 +160,8 @@ Reset Initial.
 \end{coq_eval}
 
 \begin{Warnings}
-\item {\tt Warning: {\ident$_i$} cannot be defined.}\\
+\item {\tt Warning: {\ident$_i$} cannot be defined.}
+
   It can happen that the definition of a projection is impossible.
   This message is followed by an explanation of this impossibility.
   There may be three reasons:
@@ -170,7 +171,7 @@ Reset Initial.
    \item The body of {\ident$_i$} uses an incorrect elimination for
      {\ident} (see sections \ref{Fixpoint} and \ref{Caseexpr}).
    \item The type of the projections {\ident$_i$} depends on previous
-   projections which themselves couldn't be defined.\\
+   projections which themselves couldn't be defined.
    \end{enumerate}  
 \end{Warnings}     
 
@@ -830,7 +831,9 @@ contextual implicit arguments must be considered or not (see sections
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example*}
-Inductive list (A:Set) : Set := nil : list A | cons : A -> list A -> list A.
+Inductive list (A:Set) : Set := 
+  | nil : list A 
+  | cons : A -> list A -> list A.
 \end{coq_example*}
 \begin{coq_example}
 Implicit Arguments cons.
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index cf918484d..9d284fa54 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -1091,7 +1091,8 @@ Fixpoint plus (n m:nat) {struct m} : nat :=
 The ordinary match operation on natural numbers can be mimicked in the
 following way.
 \begin{coq_example*}
-Fixpoint nat_match (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C :=
+Fixpoint nat_match 
+  (C:Set) (f0:C) (fS:nat -> C -> C) (n:nat) {struct n} : C :=
   match n with
   | O => f0
   | S p => fS p (nat_match C f0 fS p)
diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex
index aa80bcb5a..686e60e7d 100644
--- a/doc/RefMan-ide.tex
+++ b/doc/RefMan-ide.tex
@@ -83,6 +83,7 @@ Finally, notice that these navigation buttons are also available in
 the menu, where their keyboard shortcuts are given.
 
 \section{Try tactics automatically}
+\label{sec:trytactics}
 
 The menu \texttt{Try Tactics} provides some features for automatically
 trying to solve the current goal using simple tactics. If such a
@@ -93,6 +94,13 @@ turn. This wizard is also available as a tool button, with a light
 bulb shape.  The set of tactics tried by the wizard is customizable in
 the preferences.
 
+These tactics are general ones, in particular they do not refer to
+particular hypotheses. You may also try specific tactics related to
+the goal or one of the hypotheses, by clicking with the right mouse
+button one the goal or the considered hypothesis. This is the
+``contextual menu on goals'' feature, that may be disabled in the
+preferences if undesirable.
+ 
 \section{Vernacular commands, templates}
 
 The \texttt{Templates} menu allows to use shortcuts to insert
@@ -148,10 +156,32 @@ TODO: \verb|Next error| !
 
 \section{Customizations}
 
-Menu \texttt{Edit/Preferences}.
+You may customize your environment using menu
+\texttt{Edit/Preferences}. A new window will be displayed, with
+several customization sections presented as a notebook. 
+
+The first section is the select the text font used for scripts, goal
+and message windows. 
+
+The second section is devoted to file management: you may
+configure automatic saving of files, by periodically saving the
+contents into files named \verb|#f#| for each opened file
+\verb|f|. You may also activate the \emph{revert} feature: in case a
+opened file is modified on the disk by a third party, \coqide{} may read
+it again for you. Note that in the case you edited that same file, you
+will be prompt to choose to either discard your changes or not.
+
+The \verb|Externals| section allows to customize the external commands
+for compilation, printing, web browsing. In the browser command, you
+may use \verb|%s| to denote the URL to open, for example: %
+\verb|mozilla -remote "OpenURL(%s)"|. 
 
-auto save, auto revert, delays
+The \verb|Tactics Wizard| section allows to defined the set of tactics
+that should be tried, in sequence, to solve the current goal.
 
+The last section is for miscellaneous boolean settings, such as the
+``contextual menu on goals'' feature presented in
+Section~\ref{sec:trytactics}. 
 
 % $Id$ 
 
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index be1be5ca0..38ab55515 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -386,7 +386,8 @@ provided.
 
 \begin{coq_example*}
 Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
-Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := exist2 : (x:A) (_:P x) (_:Q x).
+Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := 
+  exist2 : (x:A) (_:P x) (_:Q x).
 \end{coq_example*}
 
 A ``strong (dependent) sum'' \verb+{x:A & (P x)}+ may be also defined,
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index 404ca5f78..4c214b1f8 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -489,7 +489,8 @@ types. He is also the maintainer of the non-domain specific automation
 tactics.
 
 Benjamin Monate is the developer of the \CoqIde{} graphical
-interface with contributions by Claude Marché.
+interface with contributions by Jean-Christophe Filliâtre, Pierre
+Letouzey and Claude Marché.
 
 Claude Marché coordinated the update of the Reference Manual for
  \Coq{} V8.0.