From 7a14c3a1f53adca3cd50bce75f9677460a4d2a1a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Mon, 16 May 2011 15:09:09 +0000 Subject: Update docstrings --- doc/PG-adapting.texi | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'doc/PG-adapting.texi') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 513bdbbe..f689c654 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -2835,11 +2835,15 @@ automatically be prefixed by the current proof assistant symbol. @c TEXI DOCSTRING MAGIC: defpgcustom @deffn Macro defpgcustom Define a new customization variable @var{-sym} for the current proof assistant.@* +This is intended for defining settings which are useful for any prover, +but which the user may require different values of across provers. + The function proof-assistant- is also defined, which can be used in the generic portion of Proof General to access the value for the current prover. -Arguments as for @samp{defcustom}, which see. -Usage: (defpgcustom SYM &rest @var{args}). +Arguments are as for @samp{defcustom}, which see. If a :group argument is +not supplied, the setting will be added to the internal settings for the +current prover (named -config). @end deffn In specific instances of Proof General, the macro @code{defpgdefault} -- cgit v1.2.3