diff options
| author | Thomas Kleymann | 1998-11-10 16:00:47 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-11-10 16:00:47 +0000 |
| commit | 7125b1fb6a1a1bec02986fd9340b3ecb31b999e7 (patch) | |
| tree | 129c279a3ee5e3b4f6f4dff13be42ce5ce5b1f6d | |
| parent | ffdefe0319d76aa039ab91f193ed2e244f6bc509 (diff) | |
(briefly) documented problem with sections in Coq
| -rw-r--r-- | doc/NewDoc.texi | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index cdbab281..1f49dee9 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -1677,7 +1677,9 @@ provers you need. After a @code{Discharge}, retraction ought to only be possible back to the first declaration/definition which is discharged. However, LEGO -Proof General does not know that Discharge has such a non-local effect. +Proof General does not know that @code{Discharge} has such a non-local +effect. See @ref{Granularity of atomic command sequences} for a proposal +on how to fix this bug. @strong{Workaround:} retract back to the first declaration/definition which is discharged. @@ -1720,6 +1722,9 @@ Thus, user-defined tactics cannot be retracted. @strong{Workaround:} You may need to retract to the start of the proof. +@unnumberedsubsec Sections + +The Coq Proof General does not know about Coq's section mechansim. @node Bugs specific to Isabelle Proof General @section Bugs specific to Isabelle Proof General @@ -1748,12 +1753,12 @@ General. Please send us contributions to this wish list, or better still, offers to implement something from it! @menu -* Granularity of Atomic Command Sequences:: +* Granularity of atomic command sequences:: * Browser mode for script files and theories:: @end menu -@node Granularity of Atomic Command Sequences -@section Granularity of Atomic Commands +@node Granularity of atomic command sequences +@section Granularity of atomic command sequences @c @cindex Granularity of Atomic Sequences @c @cindex Retraction @c @cindex Goal |