From deb151305196ca65b7abe51b530872aa33cc66f1 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 4 Oct 2010 13:54:05 +0000
Subject: Fully remove section for Coq-specific variables (coq-version-is-*

---
 doc/ProofGeneral.texi | 24 ------------------------
 1 file changed, 24 deletions(-)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index b55951c7..049a4cf5 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -3890,7 +3890,6 @@ assistant.  It supports most of the generic features of Proof General.
 
 @menu
 * Coq-specific commands::
-* Coq-specific variables::
 * Editing multiple proofs::
 * User-loaded tactics::
 * Holes feature::
@@ -3919,29 +3918,6 @@ Inserts ``End <section-name>.'' (this should work well with nested sections).
 Prompts for a SearchIsos argument.
 @end table
 
-@c da: I think this section is obsolete now, Pierre?
-
-@c @node Coq-specific variables
-@c @section Coq-specific variables
-@c @kindex coq-version-is-V8-0
-@c @kindex coq-version-is-V8-1
-
-@c The variable
-@c @lisp
-@c   coq-version-is-Vx
-@c @end lisp
-@c (where x is 8-0 or 8-1) is used to force version of Coq, if it is t,
-@c then Coq is considered in version x. ProofGeneral sets it automatically
-@c by doing the following shell command: 
-@c @lisp
-@c   (concat coq-prog-name "-v")
-@c @end lisp
-
-@c So you should not have to set this variable unless you have problems
-@c with different versions of Coq, you can set to t the variable
-@c corresponding to the version you are using in your config file (before
-@c ProofGeneral is loaded) and ProofGeneral won't override it.
-
 
 @node Editing multiple proofs
 @section Editing multiple proofs
-- 
cgit v1.2.3