Generic monadic indentation + specifically ext-lib / Compcert + doc.

This a generalization of PR#451 proposed by @Chobbes.

Since these syntax are not completely universal (and not builtin in
coq), the idea is to make the syntax customizable, especially to make
it possible to disable it.

NOTE: to make the Compcert syntax supported I had to refine the smie
lexer so that the ";" token was emitted as a fllback instead of ";
tactic".

NOTE2: I had to make the coq-user-token and coq-monadic-tokens be
tested ON THE RESULT of smie-coq-backward-token.

1 files changed, 16 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4195c26a..2b686029 100644
--- a/CHANGES
+++ b/CHANGES
@@ -60,6 +60,22 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
     
     The set of tokens can be seen in variable smie-grammar.
 
+*** Indentation of monadic notations.
+    Using the extensibility for indentation described above we provide
+    a way to define your own monadic operators using the
+    coq-smie-monadic-tokens in the same spirit as coq-smie-user-tokens
+    above.
+
+    By default two well established syntax are supported:
+
+       x <- e ;;
+       e
+
+     and 
+
+       do x <- e ;
+       e
+
 *** Clickable Hypothesis in goals buffer to copy/paste hyp names
 
     Clicking on a hyp name in goals buffer with button 2 copies its