diff options
Diffstat (limited to 'checker/safe_typing.ml')
| -rw-r--r-- | checker/safe_typing.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 11cd742b..e3640c37 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -40,7 +42,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - CErrors.error "Needs option -impredicative-set." + CErrors.user_err Pp.(str "Needs option -impredicative-set.") | _ -> () end; () @@ -61,7 +63,7 @@ let check_imports f caller env needed = let actual_stamp = lookup_digest env dp in if stamp <> actual_stamp then report_clash f caller dp with Not_found -> - error ("Reference to unknown module " ^ (DirPath.to_string dp)) + user_err Pp.(str ("Reference to unknown module " ^ (DirPath.to_string dp))) in Array.iter check needed @@ -89,6 +91,6 @@ let import file clib univs digest = let unsafe_import file clib univs digest = let env = !genv in if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps - else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps; + else check_imports (user_err ~hdr:"unsafe_import") clib.comp_name env clib.comp_deps; check_engagement env clib.comp_enga; full_add_module clib.comp_name clib.comp_mod univs digest |