diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-03-17 11:50:16 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-03-17 11:50:16 +0000 |
| commit | 95c1e5b08b8486145ed72bdc96b62885ca495eda (patch) | |
| tree | 1db93c0441a3b835166de65459e6c76d0495c0ea /FAQ | |
| parent | 10a5213f635c40cdbf4316565818ca10ee6efd58 (diff) | |
Mention coq-utf-safe
Diffstat (limited to 'FAQ')
| -rw-r--r-- | FAQ | 11 |
1 files changed, 9 insertions, 2 deletions
@@ -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.) ----------------------------------------------------------------- |