fix documentation issues, and add entry to change log

2 files changed, 22 insertions, 9 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 3e50a13e9e..c1755e9271 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -154,6 +154,16 @@ Tools
 - A new `-bytecode-compiler` flag for `coqc` and `coqtop` controls whether
   conversion can use the VM. The default value is `yes`.
 
+- CoqIDE now supports input for Unicode characters. For example, typing
+  "\alpha" then the "Shift+Space" will insert the greek letter alpha.
+  In fact, typing the prefix string "\a" is sufficient.
+  A larger number of default bindings are provided, following the latex
+  naming convention. Bindings can be customized, either globally, or on a
+  per-project basis, with the requirement is that keys must begin with a
+  backslash and contain no space character. Bindings may be assigned custom
+  priorities, so that prefixes resolve to the most convenient bindings.
+  The documentation pages for CoqIDE provides further details.
+
 Standard Library
 
 - Added lemmas about monotonicity of `N.double` and `N.succ_double`, and about
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index 6f48daf208..97d86943fb 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -284,15 +284,18 @@ and place it in the same folder as ``coqide.keys``. On Linux, this would be
 the folder ``~/.config/coq``. The file `coqide.bindings` should contain one
 binding per line, in the form ``\key value``, followed by an optional priority
 integer. (The key and value should not contain any space character.)
-Here is an example configuration file:
 
-```
-\par ||
-\pi π 1
-\le ≤ 1
-\lambda λ 2
-\lambdas λs
-```
+.. example::
+
+   Here is an example configuration file:
+
+   ::
+
+     \par ||
+     \pi π 1
+     \le ≤ 1
+     \lambda λ 2
+     \lambdas λs
 
 Above, the priority number 1 on ``\pi`` indicates that the prefix ``\p``
 should resolve to ``\pi``, and not to something else (e.g. ``\par``).
@@ -309,7 +312,7 @@ Each of the file tokens provided may consists of one of:
  -  the token ``local``, which resolves to the `coqide.bindings` file
     stored in the user configuration directory.
 
-.. remark::
+.. warning::
 
    If a filename other than the first one includes a "~" to refer
    to the home directory, it won't be expanded properly. To work around that