aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/himsg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/himsg.ml')
-rw-r--r--vernac/himsg.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 189c47aab..7b1a948ed 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -899,11 +899,11 @@ let explain_not_match_error = function
quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst)
let explain_signature_mismatch l spec why =
- str "Signature components for label " ++ pr_label l ++
+ str "Signature components for label " ++ Label.print l ++
str " do not match:" ++ spc () ++ explain_not_match_error why ++ str "."
let explain_label_already_declared l =
- str "The label " ++ pr_label l ++ str " is already declared."
+ str "The label " ++ Label.print l ++ str " is already declared."
let explain_application_to_not_path _ =
strbrk "A module cannot be applied to another module application or " ++
@@ -933,11 +933,11 @@ let explain_not_equal_module_paths mp1 mp2 =
str "Non equal modules."
let explain_no_such_label l =
- str "No such label " ++ pr_label l ++ str "."
+ str "No such label " ++ Label.print l ++ str "."
let explain_incompatible_labels l l' =
str "Opening and closing labels are not the same: " ++
- pr_label l ++ str " <> " ++ pr_label l' ++ str "!"
+ Label.print l ++ str " <> " ++ Label.print l' ++ str "!"
let explain_not_a_module s =
quote (str s) ++ str " is not a module."
@@ -946,19 +946,19 @@ let explain_not_a_module_type s =
quote (str s) ++ str " is not a module type."
let explain_not_a_constant l =
- quote (pr_label l) ++ str " is not a constant."
+ quote (Label.print l) ++ str " is not a constant."
let explain_incorrect_label_constraint l =
str "Incorrect constraint for label " ++
- quote (pr_label l) ++ str "."
+ quote (Label.print l) ++ str "."
let explain_generative_module_expected l =
- str "The module " ++ pr_label l ++ str " is not generative." ++
+ str "The module " ++ Label.print l ++ str " is not generative." ++
strbrk " Only components of generative modules can be changed" ++
strbrk " using the \"with\" construct."
let explain_label_missing l s =
- str "The field " ++ pr_label l ++ str " is missing in "
+ str "The field " ++ Label.print l ++ str " is missing in "
++ str s ++ str "."
let explain_include_restricted_functor mp =