diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2003-02-05 12:57:00 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2003-02-05 12:57:00 +0000 |
| commit | f59be791218fca2f3a0a82a5d5db4a16ce49f33f (patch) | |
| tree | 61edacc61dcffb4ab8aa91d55b678546a4954357 /doc | |
| parent | de1eb0269e1d678f79368c1438133111e0655fd5 (diff) | |
Added a paragraph in the documentation for the variable coq-version-is-V74.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index a376e863..29afa179 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3243,6 +3243,25 @@ it by doing the shell command: If you have problems with different versions of Coq, you can set this variable in your config file (before ProofGeneral is loaded). +@kindex coq-version-is-V7 + +The variable +@lisp + coq-version-is-V74 +@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 + +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 |