From f36f1d07ee0b9b40d54b9fece942b00e8e5e5d50 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Mar 2015 18:44:33 +0100
Subject: 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
---
 doc/faq/FAQ.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/faq')

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?}
 
-- 
cgit v1.2.3