added little doc for holes.

1 files changed, 63 insertions, 60 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 31409da4..1744f562 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3010,7 +3010,7 @@ with the path @code{.../dir/theories/} added in the libraries path
 
 (* 
  Local Variables: 
- coq-prog-name: "coqtop -emacs -full -I ../theories"
+ coq-prog-name: "coqtop -emacs -I ../theories"
  End:
 *)
 @end lisp
@@ -3049,41 +3049,16 @@ any other buffer local variable.  @inforef{File Variables,
 A very useful package of Emacs supports automatic expansions of
 abbreviations as you type, @inforef{Abbrevs, ,(xemacs)}.
 
-Proof General has no special support for abbreviations, we just mention
-it here to encourage its use.  For example, the proof assistant Coq has
-many command strings that are long, such as ``Reflexivity,''
-``Inductive,'' ``Definition'' and ``Discriminate.''  Here is the
-Coq Proof General author's suggested abbreviations for Coq:
+Proof General has no special support for abbreviations (except for coq,
+see Note below), we just mention it here to encourage its use.  For
+example, the proof assistant Coq has many command strings that are long,
+such as ``reflexivity,'' ``Inductive,'' ``Definition'' and
+``Discriminate.''  Here is a part of the Coq Proof General
+abbreviations:
 @lisp
-"assn" 0 "Assumption"
-"ax" 0 "Axiom"
-"coern" 0 "Coercion"
-"cofixpt" 0 "CoFixpt"
-"coindv" 0 "CoInductive"
-"constr" 0 "Constructor"
-"contradn" 0 "Contradiction"
-"defn" 0 "Definition"
-"discr" 0 "Discriminate"
-"extrn" 0 "Extraction"
-"fixpt" 0 "Fixpoint"
-"genz" 0 "Generalize"
-"hypo" 0 "Hypothesis"
-"immed" 0 "Immediate"
-"indn" 0 "Induction"
-"indv" 0 "Inductive"
-"injn" 0 "Injection"
-"intn" 0 "Intuition"
-"invn" 0 "Inversion"
-"pmtr" 0 "Parameter"
-"refly" 0 "Reflexivity"
-"rmk" 0 "Remark"
-"specz" 0 "Specialize"
-"symy" 0 "Symmetry"
-"thm" 0 "Theorem"
-"transpt" 0 "Transparent"
-"transy" 0 "Transitivity"
-"trivial" 0 "Trivial"
-"varl" 0 "Variable"
+"abs" "absurd "
+"ap" "apply "
+"as" "assumption"
 @end lisp
 
 The above list was taken from the file that Emacs saves between
@@ -3096,6 +3071,9 @@ mode you can expand an abbreviation by pressing @kbd{C-x '}
 (@code{expand-abbrev}). See the Emacs manual for more details.
 
 
+@b{Note:} Coq ProofGeneral has a special experimental feature called
+"Holes". It makes use of emacs abbreviation mechanism. @xref{Holes
+feature}, for details.
 
 
 
@@ -3221,6 +3199,7 @@ but does not have integrated file management or proof-by-pointing yet.
 * Coq-specific variables::
 * Editing multiple proofs::
 * User-loaded tactics::
+* Holes feature::
 @end menu
 
 
@@ -3248,41 +3227,41 @@ Prompts for a SearchIsos argument.
 
 @node Coq-specific variables
 @section Coq-specific variables
-@kindex coq-version-is-V7
+@kindex coq-version-is-Vx
 
 The variable
 @lisp
-  coq-version-is-V7
+  coq-version-is-Vx
 @end lisp
-is used to force version of Coq, if it is t, then Coq is considered in
-version 7, if it is nil, then Coq is considered in an old version
-(V6). You should not have to set this variable, since ProofGeneral sets
-it by doing the shell command:
+(where x is 6, 74, 7 or 8) is used to force version of Coq, if it is t,
+then Coq is considered in version x. You should not have to set this
+variable, since ProofGeneral sets it by doing the shell command:
 @lisp
   (concat coq-prog-name "-v")
 @end lisp
 
-If you have problems with different versions of Coq, you can set this
-variable in your config file (before ProofGeneral is loaded).
+If you have problems with different versions of Coq, you can set to t
+the variable corresponding to the version you are using in your config
+file (before ProofGeneral is loaded).
 
 @kindex coq-version-is-V7
 
-The variable
-@lisp
-  coq-version-is-V74
-@end lisp
+@c The variable
+@c @lisp
+@c   coq-version-is-V74
+@c @end lisp
 
-(PG > 3.5pre030204) is used to force version of Coq, if it is t, then
-Coq is considered in version 7.4 (i.e. with the module system enabled),
-if it is nil, then Coq is considered in an old version (V7 or V6,
-depending on @code{coq-version-is-V7}). You should not have to set this
-variable, since ProofGeneral sets it by doing the shell command:
-@lisp
-  (concat coq-prog-name "-v")
-@end lisp
+@c (PG > 3.5pre030204) is used to force version of Coq, if it is t, then
+@c Coq is considered in version 7.4 (i.e. with the module system enabled),
+@c if it is nil, then Coq is considered in an old version (V7 or V6,
+@c depending on @code{coq-version-is-V7}). You should not have to set this
+@c variable, since ProofGeneral sets it by doing the shell command:
+@c @lisp
+@c   (concat coq-prog-name "-v")
+@c @end lisp
 
-If you have problems with different versions of Coq, you can set this
-variable in your config file (before ProofGeneral is loaded).
+@c If you have problems with different versions of Coq, you can set this
+@c variable in your config file (before ProofGeneral is loaded).
 
 @node Editing multiple proofs
 @section Editing multiple proofs
@@ -3350,14 +3329,16 @@ We give an example of existing commands that fit each category.
 @item @code{coq-user-state-preserving-tactics}: example: "@code{Idtac}"
 @end itemize
 
-This variables regexp string lists. See their documentations in emacs
-(@code{C-h v coq-user...})  for details on how to set them in your
+This variables are regexp string lists. See their documentations in
+emacs (@code{C-h v coq-user...})  for details on how to set them in your
 @file{.emacs} file.
 
 Here is a simple example:
 @lisp
 (setq coq-user-state-changing-commands 
-      '("MyHint" "MyRequire" "Show\\s-+Mydata"))
+      '("MyHint" "MyRequire"))
+(setq coq-user-state-preserving-commands 
+      '("Show\\s-+Mydata"))
 @end lisp
 
 The regexp character sequence @code{\\s-+} means "one or more
@@ -3371,6 +3352,28 @@ move the locked region to the proper position,
 @kbd{C-c C-v} to re-issue an erroneously back-tracked tactic without
 recording it in the script.
 
+@node Holes feature
+@section Holes feature
+
+@emph{Holes} are an experimental feature for complex expression
+editing. It is inspired from other tools, like Pcoq
+(@uref{http://www-sop.inria.fr/lemme/pcoq/index.html}). The principle is
+simple, holes are pieces of text that can be "filled" by different
+means. The new coq command insertion menu system makes use of the holes
+system. Almost all holes operations are available in the Coq/holes menu.
+
+@b{Note:} Holes make use of emacs abbreviation mechanism, it will work
+without problem if you don't have an abbrev table defined for coq in you
+config files (@code{C-h v abbrev-file-name} to see the name of the
+abbreviation file). If you already have such a table it won't be
+automatically overwritten (so that you keep your own abrreviations). But
+you must read the abbrev file given in PG/Coq sources to be able to use
+the command insertion menus. You can do the following to merge your
+abbreviations with ProofGeneral's abbreviations: @code{M-x
+read-abbrev-file}, then select the file named @code{coq-abbrev.el} in
+the ProofGeneral/coq directory. At emacs exit you will be asked if you
+want to save abbrevs, answer yes.
+
 
 @c=================================================================
 @c