diff options
-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 |