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, 23 insertions, 8 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 9717292456..2917f52c58 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -74,7 +74,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -338,8 +338,22 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
 
 type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
 
-let return_proof () =
-  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
+let return_proof ?(allow_partial=false) () =
+ let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
+ if allow_partial then begin
+  if Proof.is_done proof then begin
+    msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++
+     str" is complete, no need to end it with Admitted");
+  end;
+  let proofs = Proof.partial_proof proof in
+  let _,_,_,_, evd = Proof.proof proof in
+  let eff = Evd.eval_side_effects evd in
+  (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+      side-effects... This may explain why one need to uniquize side-effects
+      thereafter... *)
+  let proofs = List.map (fun c -> c, eff) proofs in
+    proofs, Evd.evar_universe_context evd
+ end else
   let initial_goals = Proof.initial_goals proof in
   let evd =
     let error s =
@@ -352,10 +366,9 @@ let return_proof () =
     | Proof.HasShelvedGoals ->
         error(str"Attempt to save a proof with shelved goals")
     | Proof.HasGivenUpGoals ->
-        error(str"Attempt to save a proof with given up goals")
+        error(strbrk"Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.")
     | Proof.HasUnresolvedEvar->
-        error(str"Attempt to save a proof with existential " ++
-              str"variables still non-instantiated") in
+        error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
   let eff = Evd.eval_side_effects evd in
   let evd =
     if poly || !Flags.compilation_mode = Flags.BuildVo
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 2700e90123..9d5038a3f9 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -66,7 +66,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -99,7 +99,9 @@ val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof
 
 type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context
 
-val return_proof : unit -> closed_proof_output
+(* If allow_partial is set (default no) then an incomplete proof
+ * is allowed (no error), and a warn is given if the proof is complete. *)
+val return_proof : ?allow_partial:bool -> unit -> closed_proof_output
 val close_future_proof : feedback_id:Stateid.t ->
   closed_proof_output Future.computation -> closed_proof