Added one point + details to CHANGES.

1 files changed, 16 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index e0edeef3..38d9a6d0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -77,6 +77,15 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
     way all the time with module.notations.
      Coq > Double Hit Electric Terminator.
 
+    Note 1: Mutually exclusive with usual electric terminator.
+
+    Note 2: For french keyboard it may be convenient to map ";"
+    instead of ".":
+
+(add-hook 'proof-mode-hook
+ (lambda () (define-key coq-mode-map (kbd ";") 'coq-terminator-insert)))
+
+
 *** Indentation improvements using SMIE. Supporting bullets and { }.
     Still experimental. Please submit bugs.
 
@@ -99,6 +108,13 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
       always introduce a proof with "Proof." (or "Next Obligation"
       with Program).
 
+*** "Show" shows the (cached) state of the proof at point.
+    If Show goals (C-c C-a C-s) is performed when point is on a locked
+    region, then it shows the prover state as stored by proofgeneral
+    at this point. This works only when the command at point has been
+    processed by "next step" (otherwise coq was silent at this point
+    and nothing were cached).
+
 *** Minor parsing fixes
 *** Windows resizing fixed