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

1 files changed, 1 insertions, 1 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?}