aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES16
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