diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index c02b90916..6c963bf70 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -341,7 +341,7 @@ 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_done proof 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; |