diff options
Diffstat (limited to 'kernel/opaqueproof.ml')
| -rw-r--r-- | kernel/opaqueproof.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index d0593c0e0..502a10113 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -36,12 +36,11 @@ let empty_opaquetab = { (* hooks *) let default_get_opaque dp _ = - CErrors.error - ("Cannot access opaque proofs in library " ^ DirPath.to_string dp) + CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp]) let default_get_univ dp _ = - CErrors.error - ("Cannot access universe constraints of opaque proofs in library " ^ - DirPath.to_string dp) + CErrors.user_err (Pp.pr_sequence Pp.str [ + "Cannot access universe constraints of opaque proofs in library "; + DirPath.to_string dp]) let get_opaque = ref default_get_opaque let get_univ = ref default_get_univ |