diff options
| author | Thomas Kleymann | 1998-11-05 16:25:17 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-11-05 16:25:17 +0000 |
| commit | 941138860e59812bdfb5475217479592e8ca3284 (patch) | |
| tree | 990e38b61a6ee56afaa578482ed7bfd2c83c6c96 /doc | |
| parent | 8bbd767323c5fc14e5f22991e2c800dffd6366da (diff) | |
completed chapter on Known bugs. However section on Isabelle Proof
General specific bugs is still missing.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/NewDoc.texi | 7 | ||||
| -rw-r--r-- | doc/notes.txt | 2 |
2 files changed, 7 insertions, 2 deletions
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index 157bc477..1af8d002 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -1311,6 +1311,7 @@ let us know by sending a note to @code{proofgen@@dcs.ed.ac.uk}. @menu * Bugs at the generic level:: * Bugs specific to LEGO Proof General:: +* Bugs specific to Coq Proof General:: @end menu @node Bugs at the generic level @@ -1370,8 +1371,12 @@ that all proofs are terminated with a proper @samp{Save} command. a proof. If you forget one, you should retract to a point before the offending proof development. +@node Bugs specific to Coq Proof General +@section Bugs specific to Coq Proof General - +The collection of tactics which Proof General is aware of is hard-wired. +Thus, user-defined tactics cannot be retracted. +@strong{Workaround:} You may need to retract to the start of the proof. @node Plans and ideas @appendix Plans and ideas diff --git a/doc/notes.txt b/doc/notes.txt index fd32d00b..dfc585d9 100644 --- a/doc/notes.txt +++ b/doc/notes.txt @@ -75,7 +75,7 @@ Suggestion for outline of improved documentation. APPENDIX A. Obtaining and installing the software [da] - B. Known bugs [tms] + B. Known bugs [done] C. Future ideas and plans [da] |