diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2010-09-01 13:34:37 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2010-09-01 13:34:37 +0000 |
| commit | c1955a6fa62b94b1906a199638caf293f29319a8 (patch) | |
| tree | 37a6c650c07539b1686d02ad7bc3876b0627efca /CHANGES | |
| parent | 06fb36588deb414cbe62699dc8ec2292aa9c8a71 (diff) | |
Fixed bug #346. Coq code was using proof-ids-to-regexp on regexp
instead of pure strings.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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-<c,p,o,b,a> are now available in goal buffer. ** Notable internal changes |