diff options
author | 2003-12-16 16:07:54 +0000 | |
---|---|---|
committer | 2003-12-16 16:07:54 +0000 | |
commit | a3281b10a5ec5721eac591ef5cfe273238d2e377 (patch) | |
tree | b4d53b4c5a649ba9358543d435a7719ab0da50de | |
parent | 6942f889bfe68b308744a01cc079403e872b4925 (diff) |
coqide menus on golas
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8403 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/Makefile | 4 | ||||
-rw-r--r-- | doc/RefMan-ext.tex | 9 | ||||
-rw-r--r-- | doc/RefMan-gal.tex | 3 | ||||
-rw-r--r-- | doc/RefMan-ide.tex | 34 | ||||
-rwxr-xr-x | doc/RefMan-lib.tex | 3 | ||||
-rwxr-xr-x | doc/RefMan-pre.tex | 3 |
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. |