diff options
| author | Matthieu Sozeau | 2016-11-08 09:00:13 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-08 09:00:13 +0100 |
| commit | cadb9e6614a1e72bf18f80acf0aabaeed4e9f057 (patch) | |
| tree | d1e81c4d456660e94ca055604bfe47564ef260d3 | |
| parent | 3bc8d841148da0cf1db5b9b896f28c3285d4f5db (diff) | |
Rewording from Enrico
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 8f75353bb3..4f4f404422 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1098,8 +1098,9 @@ over 100 contributions integrated. The main user visible changes are: can outperform the previous version by an order of magnitude, by Jacques-Henri Jourdan. \item In CoqIDE and other asynchronous interfaces, more fine-grained - asynchronous processing and error reporting by Enrico Tassi (ability - to jump to any error in the document). + asynchronous processing and error reporting by Enrico Tassi. In + asynchronous mode {\Coq} is now capable of recovering from errors + and continue processing the document. \item More access to the proof engine features from Ltac: goal management primitives, range selectors and a {\tt typeclasses eauto} engine handling multiple goals and multiple successes, by |