diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2001-08-28 17:00:40 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2001-08-28 17:00:40 +0000 |
| commit | 13b195a928387765b2ae8317d28a0cf36d225596 (patch) | |
| tree | c196a8aa6c2b45271215422e006ca9221497ad75 /doc | |
| parent | 242fa6a6b9e11d7c41537025e824ae546915c648 (diff) | |
added something in the doc about coq-version-is-V7.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 8c5dbc63..9b2656db 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3196,6 +3196,7 @@ but does not have integrated file management or proof-by-pointing yet. @menu * Coq-specific commands:: +* Coq-specific variables:: * Editing multiple proofs:: * User-loaded tactics:: @end menu @@ -3223,6 +3224,25 @@ Inserts ``End <section-name>.'' (this should work well with nested sections). Prompts for a SearchIsos argument. @end table +@node Coq-specific variables +@section Coq-specific variables +@kindex coq-version-is-V7 + +The variable +@lisp + coq-version-is-V7 +@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: +@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). + @node Editing multiple proofs @section Editing multiple proofs |