From c1955a6fa62b94b1906a199638caf293f29319a8 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 1 Sep 2010 13:34:37 +0000 Subject: Fixed bug #346. Coq code was using proof-ids-to-regexp on regexp instead of pure strings. --- CHANGES | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 7809d0c4..78b72bdc 100644 --- a/CHANGES +++ b/CHANGES @@ -70,7 +70,6 @@ *** "Movie" output: export an annotated buffer in XML Basic movie output for Proviola, see http://mws.cs.ru.nl/proviola - ** Isabelle/Isar changes *** Support undo back into completed proofs (linear_undo). @@ -84,13 +83,14 @@ *** Isabelle Settings now organised in sub-menus - ** Coq changes *** Only supports Coq 8.1+, support for earlier versions dropped. *** Holes mode can be turned on/off and has its own minor mode +*** Some keyboard shortcuts are now available in goals buffer + C-c C-a C- are now available in goal buffer. ** Notable internal changes -- cgit v1.2.3