admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)

- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
  - the quick chain can stock "Admitted" jobs in .vio files
  - the vio2vo step checks the jobs but does not stock the result
    in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
  used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
  use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
  find TestSuite.admit

3 files changed, 2 insertions, 14 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 5a66910722..589933578a 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1465,7 +1465,7 @@ You can use the {\tt Clear} command.
 \Question{How can use a proof which is not finished?}
 
 You can use the {\tt Admitted} command to state your current proof as an axiom.
-You can use the {\tt admit} tactic to omit a portion of a proof.
+You can use the {\tt give\_up} tactic to omit a portion of a proof.
 
 \Question{How can I state a conjecture?}
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 32f94abf7a..556a2dab58 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -432,7 +432,7 @@ the search results via the command
 {\tt Add Search Blacklist "substring1"}.
 A lemma whose fully-qualified name contains any of the declared substrings
 will be removed from the search results.
-The default blacklisted substrings are {\tt "\_admitted"
+The default blacklisted substrings are {\tt 
   "\_subproof" "Private\_"}. The command {\tt Remove Search Blacklist
   ...} allows expunging this blacklist.
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 52f32d0c7d..2eebac18e6 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1439,18 +1439,6 @@ a hypothesis or in the body or the type of a local definition.
 
 \end{Variants}
 
-\subsection{\tt admit}
-\tacindex{admit}
-\label{admit}
-
-The {\tt admit} tactic ``solves'' the current subgoal by an
-axiom. This typically allows temporarily skipping a subgoal so as to
-progress further in the rest of the proof. To know if some proof still
-relies on unproved subgoals, one can use the command {\tt Print
-Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
-have names of the form {\ident}\texttt{\_admitted} possibly followed
-by a number.
-
 \subsection{\tt absurd \term}
 \tacindex{absurd}
 \label{absurd}