diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2010-09-09 16:58:33 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2010-09-09 16:58:33 +0000 |
| commit | 6dabc28114f0ee2ba03b79c4bdd313154cab8d30 (patch) | |
| tree | c2a4eeb307f2756517acc7bc3678f640f8bad09d /CHANGES | |
| parent | 062204d996652b87ee1398c630937eda69b929c0 (diff) | |
Fixed the cleaning of goals buffer when proof completed
+ fixed the refreshing of modeline goal number display.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -97,11 +97,14 @@ persistent buffer (for later use), use Coq/Store response or Coq/Store goal. -*** bug fixes +*** bug fixes, bugs - Three panes mode: "window would be too small" error fixed. - Indentation: several error fixed. If you want to indent tactics inside "Instance" or "Add Parametric Relation" etc, please put - "Proof." before the tactics. + "Proof." before the tactics, there is no way for emacs to guess + wether these commands initiate new goals or not. + - coq prog args permanent settings is working again + - when a proof is completed, the goals buffer is cleared again. ** Notable internal changes |