diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-08-19 12:03:39 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-08-19 12:03:39 +0000 |
| commit | 62e815d604cd8c1f53c94b34e876259c32839cf2 (patch) | |
| tree | 83907b0dfd4986b8b540cb3c5bf71dd2bc50ef91 /doc/PG-adapting.texi | |
| parent | d46f608df12be9b6ebf07122b6f50a40abc99078 (diff) | |
pg-topterm-char -> pg-topterm-regexp
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 4 |
1 files 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) |