diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-09 09:48:48 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-09 09:48:53 +0200 |
| commit | 73daf37ccc7a44cd29c9b67405111756c75cb26a (patch) | |
| tree | 5ebc5d9e3e27eb34f5714a33ba957fce621b3659 /proofs/proof_global.ml | |
| parent | b6edcae7b61ea6ccc0e65223cecb71cab0dd55cc (diff) | |
Remove misleading warning (Close #4365)
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f777e6ed7..3e06294e6 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 |