From 03d1fa42c17896cb9d767b509e05bd0db78cb7d2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 17 Jun 2015 10:34:08 +0200
Subject: Doc: Workers do check for guardedness before sending proofs back

---
 doc/refman/AsyncProofs.tex | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 797bf24340..47dc1ac1a6 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -18,13 +18,11 @@ on small sets of short files.
 This feature has some technical limitations that may make it unsuitable for
 some use cases.
 
-For example, in interactive mode, errors coming from the kernel of Coq are
-signaled late.  The most notable type of errors belonging to this category are
-universe inconsistencies or unsatisfied guardedness conditions for fixpoints
-built using tactics.
+For example, in interactive mode, some errors coming from the kernel of Coq
+are signaled late.  The type of errors belonging to this category
+are universe inconsistencies.
 
-Last, at the time of writing, only opaque proofs (ending with \texttt{Qed}) can be
-processed asynchronously.
+Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously.
 
 \subsection{Proof annotations}
 
-- 
cgit v1.2.3