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

2 files changed, 1 insertions, 4 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index d2971552d..50f853f0e 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -22,9 +22,6 @@ Inductive True : Prop :=
 (** [False] is the always false proposition *)
 Inductive False : Prop :=.
 
-(** [proof_admitted] is used to implement the admit tactic *)
-Axiom proof_admitted : False.
-
 (** [not A], written [~A], is the negation of [A] *)
 Definition not (A:Prop) := A -> False.
 
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 4894eba4b..0efb8744d 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -23,4 +23,4 @@ Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
 Declare ML Module "recdef_plugin".
 (* Default substrings not considered by queries like SearchAbout *)
-Add Search Blacklist "_admitted" "_subproof" "Private_".
+Add Search Blacklist "_subproof" "Private_".