diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-05-16 15:09:09 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-05-16 15:09:09 +0000 |
| commit | 7a14c3a1f53adca3cd50bce75f9677460a4d2a1a (patch) | |
| tree | fd5e2648b747bfe04276ee0218b4b74083bd11a2 /doc/PG-adapting.texi | |
| parent | b7c2185ba7eec3a68c7e49f114eddf5ba92eb594 (diff) | |
Update docstrings
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 8 |
1 files changed, 6 insertions, 2 deletions
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 <PA>@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-<SYM> 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 <PA>-config). @end deffn In specific instances of Proof General, the macro @code{defpgdefault} |