aboutsummaryrefslogtreecommitdiffhomepage
path: root/FAQ
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2007-03-17 11:50:16 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2007-03-17 11:50:16 +0000
commit95c1e5b08b8486145ed72bdc96b62885ca495eda (patch)
tree1db93c0441a3b835166de65459e6c76d0495c0ea /FAQ
parent10a5213f635c40cdbf4316565818ca10ee6efd58 (diff)
Mention coq-utf-safe
Diffstat (limited to 'FAQ')
-rw-r--r--FAQ11
1 files changed, 9 insertions, 2 deletions
diff --git a/FAQ b/FAQ
index 34962cef..e659e774 100644
--- a/FAQ
+++ b/FAQ
@@ -55,13 +55,20 @@ A. This is caused by UTF-8 support in recent linuxes with glibc 2.2 or later
but I haven't tried this.
- UPDATE for PG Version 3.6:
+ UPDATE for PG Version 3.6pre and 3.7:
- Some provers have a Unicode-safe interaction mode. You can set
+ Some provers now have a Unicode-safe interaction mode. You can set
`proof-shell-unicode' to try to enable communication with the
prover which does not use non-ASCII 8-bit characters for markup.
This is supported in Isabelle > Isabelle 2005. Then the locale
setting will not matter.
+
+ In Coq, set coq-utf-safe by
+
+ (setq coq-utf-safe t)
+
+ in your .emacs or init.el file. (This mechanism may be integrated
+ with `proof-shell-unicode' soon.)
-----------------------------------------------------------------