From ba090c7e88c00df4d0db7e5c521bd30d4fb61ec4 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 7 Sep 2012 14:52:43 +0000 Subject: Added one point + details to CHANGES. --- CHANGES | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) 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 -- cgit v1.2.3