From 13b195a928387765b2ae8317d28a0cf36d225596 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 28 Aug 2001 17:00:40 +0000
Subject: added something in the doc about coq-version-is-V7.

---
 doc/ProofGeneral.texi | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'doc')

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
 
-- 
cgit v1.2.3