diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-29 17:47:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-12 16:49:46 +0200 |
| commit | 2f0a56562112c4bd66082fb3eafffb8cf6f03a88 (patch) | |
| tree | 2586dcdbe566519fa5325fa2551f658fbb87a700 /dev/doc | |
| parent | 55bddb4bf35fa68318aa57a5fa8a113d1fe51159 (diff) | |
[stm] Improve error messages on add/parse.
As suggested by @psteckler in #524 , we give more explicit information
about what is wrong.
We also provide some debug information for the possible dangerous case
of having the tip go out of sync with the real installed state (which
will make parsing fail if there was some changes to the parser).
We also fix a couple of typos noticed by Paul, thanks Paul.
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7e7bb9858..fe0b587b1 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -148,7 +148,7 @@ document type". This allows for a more uniform handling of printing - The main parsing entry point has also been moved to the `Stm`. Parsing is considered a synchronous operation so it will - either succeed of emit an exception. + either succeed or raise an exception. - `Feedback` is now only emitted for asynchronous operations. As a consequence, it always carries a valid stateid and the type has @@ -167,7 +167,7 @@ document type". This allows for a more uniform handling of printing ** XML Protocol ** -- The legacy `interp` call has been turned into a noop. +- The legacy `Interp` call has been turned into a noop. ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = |