From 73daf37ccc7a44cd29c9b67405111756c75cb26a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 9 Oct 2015 09:48:48 +0200
Subject: Remove misleading warning (Close #4365)

---
 proofs/proof_global.ml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f777e6ed7a..3e06294e64 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -365,10 +365,6 @@ type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.ev
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
-  if Proof.is_complete 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
-- 
cgit v1.2.3