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, 1 insertions, 12 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1ffc0519fe..891e2dba51 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -25,13 +25,9 @@ open Misctypes
 DECLARE PLUGIN "extratactics"
 
 (**********************************************************************)
-(* admit, replace, discriminate, injection, simplify_eq               *)
+(* replace, discriminate, injection, simplify_eq                      *)
 (* cutrewrite, dependent rewrite                                      *)
 
-TACTIC EXTEND admit
-  [ "admit" ] -> [ admit_as_an_axiom ]
-END
-
 let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
   Tacticals.New.tclWITHHOLES false
     (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ad6684e25b..b1559da33f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4411,11 +4411,6 @@ let tclABSTRACT name_op tac =
   in
   abstract_subproof s gk tac
 
-let admit_as_an_axiom =
-  Proofview.tclUNIT () >>= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
-  simplest_case (Coqlib.build_coq_proof_admitted ()) <*>
-  Proofview.mark_as_unsafe
-
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.nf_enter begin fun gl ->
   try
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6025883fe6..eea4956214 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -393,8 +393,6 @@ val unify           : ?state:Names.transparent_state -> constr -> constr -> unit
 
 val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
-val admit_as_an_axiom : unit Proofview.tactic
-
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> tactic