diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b57001237..0a7aa7862 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -752,15 +752,15 @@ let _ = () with e -> if is_unsafe "proof" then begin - mSGNL [< 'sTR"Error: checking of theorem " ; pr_id s ; - 'sPC ; 'sTR"failed" ; - 'sTR"... converting to Axiom" >]; + mSGNL [< 'sTR "Warning: checking of theorem "; pr_id s; + 'sPC; 'sTR "failed"; + 'sTR "... converting to Axiom" >]; delete_proof s; parameter_def_var (string_of_id s) com end else - errorlabstrm "vernacentries__TheoremProof" - [< 'sTR"checking of theorem " ; pr_id s ; 'sPC ; - 'sTR"failed... aborting" >]) + errorlabstrm "Vernacentries.TheoremProof" + [< 'sTR "checking of theorem "; pr_id s; 'sPC; + 'sTR "failed... aborting" >]) | _ -> bad_vernac_args "TheoremProof") let _ = |