From 62e815d604cd8c1f53c94b34e876259c32839cf2 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 19 Aug 2007 12:03:39 +0000
Subject: pg-topterm-char -> pg-topterm-regexp

---
 doc/PG-adapting.texi | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index e18a3daf..0770c2b0 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -2107,8 +2107,8 @@ subterm and proof-by-pointing markup mechanisms..
 Finishing special for a subterm markup.@*
 See doc of @samp{@code{pg-subterm-start-char}}.
 @end defvar
-@c TEXI DOCSTRING MAGIC: pg-topterm-char
-@defvar pg-topterm-char 
+@c TEXI DOCSTRING MAGIC: pg-topterm-regexp
+@defvar pg-topterm-regexp
 Annotation character that indicates the beginning of a "top" element.@*
 A "top" element may be a sub-goal to be proved or a named hypothesis,
 for example.  It is currently assumed (following @var{lego}/Coq conventions)
-- 
cgit v1.2.3