aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/safe_typing.ml6
-rw-r--r--interp/coqlib.ml2
-rw-r--r--library/libnames.ml4
-rw-r--r--library/library.ml10
-rw-r--r--library/nameops.ml4
-rw-r--r--library/nametab.ml2
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--printing/ppconstr.ml6
-rw-r--r--printing/ppvernac.ml2
-rw-r--r--printing/printer.ml4
-rw-r--r--printing/printmod.ml2
-rw-r--r--toplevel/himsg.ml16
-rw-r--r--toplevel/obligations.ml8
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/vernacentries.ml6
15 files changed, 39 insertions, 37 deletions
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 81a3cc035..ee3305167 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -13,6 +13,8 @@ open Cic
open Names
open Environ
+let pr_dirpath dp = str (DirPath.to_string dp)
+
(************************************************************************)
(*
* Global environment
@@ -52,9 +54,9 @@ let check_engagement env (expected_impredicative_set,expected_type_in_type) =
let report_clash f caller dir =
let msg =
- str "compiled library " ++ str(DirPath.to_string caller) ++
+ str "compiled library " ++ pr_dirpath caller ++
spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
- str(DirPath.to_string dir) ++ fnl() in
+ pr_dirpath dir ++ fnl() in
f msg
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 5ac718e3b..b309f26cd 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -87,7 +87,7 @@ let check_required_library d =
*)
(* or failing ...*)
errorlabstrm "Coqlib.check_required_library"
- (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.")
+ (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
(************************************************************************)
(* Specific Coq objects *)
diff --git a/library/libnames.ml b/library/libnames.ml
index cdaec6a3d..36b46ca49 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -13,7 +13,7 @@ open Names
(**********************************************)
-let pr_dirpath sl = (str (DirPath.to_string sl))
+let pr_dirpath sl = str (DirPath.to_string sl)
(*s Operations on dirpaths *)
@@ -197,7 +197,7 @@ let string_of_reference = function
let pr_reference = function
| Qualid (_,qid) -> pr_qualid qid
- | Ident (_,id) -> str (Id.to_string id)
+ | Ident (_,id) -> Id.print id
let loc_of_reference = function
| Qualid (loc,qid) -> loc
diff --git a/library/library.ml b/library/library.ml
index 4f964a051..ef621e16b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -132,7 +132,7 @@ let try_find_library dir =
try find_library dir
with Not_found ->
errorlabstrm "Library.find_library"
- (str "Unknown library " ++ str (DirPath.to_string dir))
+ (str "Unknown library " ++ pr_dirpath dir)
let register_library_filename dir f =
(* Not synchronized: overwrite the previous binding if one existed *)
@@ -474,7 +474,7 @@ and intern_library_deps libs dir m from =
and intern_mandatory_library caller from libs (dir,d) =
let digest, libs = intern_library libs (dir, None) from in
if not (Safe_typing.digest_match ~actual:digest ~required:d) then
- errorlabstrm "" (str "Compiled library " ++ str (DirPath.to_string caller) ++ str ".vo makes inconsistent assumptions over library " ++ str (DirPath.to_string dir));
+ errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir);
libs
let rec_intern_library libs (dir, f) =
@@ -567,7 +567,7 @@ let safe_locate_module (loc,qid) =
try Nametab.locate_module qid
with Not_found ->
user_err_loc
- (loc,"import_library", str (string_of_qualid qid) ++ str " is not a module")
+ (loc,"import_library", pr_qualid qid ++ str " is not a module")
let import_module export modl =
(* Optimization: libraries in a raw in the list are imported
@@ -592,7 +592,7 @@ let import_module export modl =
try Declaremods.import_module export mp; aux [] l
with Not_found ->
user_err_loc (loc,"import_library",
- str (string_of_qualid dir) ++ str " is not a module"))
+ pr_qualid dir ++ str " is not a module"))
| [] -> flush acc
in aux [] modl
@@ -604,7 +604,7 @@ let check_coq_overwriting p id =
let is_empty = match l with [] -> true | _ -> false in
if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
errorlabstrm ""
- (str "Cannot build module " ++ str (DirPath.to_string p) ++ str "." ++ pr_id id ++ str "." ++ spc () ++
+ (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
(* Verifies that a string starts by a letter and do not contain
diff --git a/library/nameops.ml b/library/nameops.ml
index 3a23ab97d..418d620c2 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -12,7 +12,7 @@ open Names
(* Identifiers *)
-let pr_id id = str (Id.to_string id)
+let pr_id id = Id.print id
let pr_name = function
| Anonymous -> str "_"
@@ -141,7 +141,7 @@ let name_max na1 na2 =
| Name _ -> na1
| Anonymous -> na2
-let pr_lab l = str (Label.to_string l)
+let pr_lab l = Label.print l
let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/nametab.ml b/library/nametab.ml
index 5b6d7cd98..621640ef9 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -523,7 +523,7 @@ let shortest_qualid_of_tactic kn =
KnTab.shortest_qualid Id.Set.empty sp !the_tactictab
let pr_global_env env ref =
- try str (string_of_qualid (shortest_qualid_of_global env ref))
+ try pr_qualid (shortest_qualid_of_global env ref)
with Not_found as e ->
if !Flags.debug then Pp.msg_debug (Pp.str "pr_global_env not found"); raise e
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 9feaea8cd..30486879e 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -453,7 +453,7 @@ let check_loaded_modfile mp = match base_mp mp with
if not (Library.library_is_loaded dp) then begin
match base_mp (Lib.current_mp ()) with
| MPfile dp' when not (DirPath.equal dp dp') ->
- err (str ("Please load library "^(DirPath.to_string dp^" first.")))
+ err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
| _ -> ()
end
| _ -> ()
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 56429410c..d15c3ee2f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -153,11 +153,11 @@ end) = struct
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
- let id = tag_ref (str (Id.to_string id)) in
+ let id = tag_ref (pr_id id) in
let sl = match List.rev (DirPath.repr sl) with
| [] -> mt ()
| sl ->
- let pr dir = tag_path (str (Id.to_string dir)) ++ str "." in
+ let pr dir = tag_path (pr_id dir) ++ str "." in
prlist pr sl
in
sl ++ id
@@ -182,7 +182,7 @@ end) = struct
let pr_reference = function
| Qualid (_, qid) -> pr_qualid qid
- | Ident (_, id) -> tag_var (str (Id.to_string id))
+ | Ident (_, id) -> tag_var (pr_id id)
let pr_cref ref us =
pr_reference ref ++ pr_universe_instance us
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index f216c599d..495719990 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1034,7 +1034,7 @@ module Make
let pr_tac_body tacdef_body =
let id, redef, body =
match tacdef_body with
- | TacticDefinition ((_,id), body) -> str (Id.to_string id), false, body
+ | TacticDefinition ((_,id), body) -> pr_id id, false, body
| TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
in
let idl, body =
diff --git a/printing/printer.ml b/printing/printer.ml
index 2e112f9ac..7c031ea53 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -777,7 +777,7 @@ let pr_assumptionset env s =
let (v, a, o, tr) = accu in
match t with
| Variable id ->
- let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
+ let var = pr_id id ++ str " : " ++ pr_ltype typ in
(var :: v, a, o, tr)
| Axiom (kn,[]) ->
let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
@@ -786,7 +786,7 @@ let pr_assumptionset env s =
let ax = safe_pr_constant env kn ++ safe_pr_ltype typ ++
cut() ++
prlist_with_sep cut (fun (lbl, ctx, ty) ->
- str " used in " ++ str (Names.Label.to_string lbl) ++
+ str " used in " ++ pr_label lbl ++
str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty))
l in
(v, ax :: a, o, tr)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index d6f847cc7..e0b1d55be 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -264,7 +264,7 @@ let nametab_register_modparam mbid mtb =
List.iter (nametab_register_body mp dir) struc
let print_body is_impl env mp (l,body) =
- let name = str (Label.to_string l) in
+ let name = pr_label l in
hov 2 (match body with
| SFBmodule _ -> keyword "Module" ++ spc () ++ name
| SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8f380830d..e21b6b41c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -822,7 +822,7 @@ let explain_not_match_error = function
| ModuleTypeFieldExpected ->
strbrk "a module type is expected"
| NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
- str "types given to " ++ str (Id.to_string id) ++ str " differ"
+ str "types given to " ++ pr_id id ++ str " differ"
| NotConvertibleBodyField ->
str "the body of definitions differs"
| NotConvertibleTypeField (env, typ1, typ2) ->
@@ -847,7 +847,7 @@ let explain_not_match_error = function
| RecordProjectionsExpected nal ->
(if List.length nal >= 2 then str "expected projection names are "
else str "expected projection name is ") ++
- pr_enum (function Name id -> str (Id.to_string id) | _ -> str "_") nal
+ pr_enum (function Name id -> pr_id id | _ -> str "_") nal
| NotEqualInductiveAliases ->
str "Aliases to inductive types do not match"
| NoTypeConstraintExpected ->
@@ -896,11 +896,11 @@ let explain_not_equal_module_paths mp1 mp2 =
str "Non equal modules."
let explain_no_such_label l =
- str "No such label " ++ str (Label.to_string l) ++ str "."
+ str "No such label " ++ pr_label l ++ str "."
let explain_incompatible_labels l l' =
str "Opening and closing labels are not the same: " ++
- str (Label.to_string l) ++ str " <> " ++ str (Label.to_string l') ++ str "!"
+ pr_label l ++ str " <> " ++ pr_label l' ++ str "!"
let explain_not_a_module s =
quote (str s) ++ str " is not a module."
@@ -909,19 +909,19 @@ let explain_not_a_module_type s =
quote (str s) ++ str " is not a module type."
let explain_not_a_constant l =
- quote (Label.print l) ++ str " is not a constant."
+ quote (pr_label l) ++ str " is not a constant."
let explain_incorrect_label_constraint l =
str "Incorrect constraint for label " ++
- quote (Label.print l) ++ str "."
+ quote (pr_label l) ++ str "."
let explain_generative_module_expected l =
- str "The module " ++ str (Label.to_string l) ++ str " is not generative." ++
+ str "The module " ++ pr_label 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 " ++ str (Label.to_string l) ++ str " is missing in "
+ str "The field " ++ pr_label l ++ str " is missing in "
++ str s ++ str "."
let explain_module_error = function
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index cac81a939..a3b973e4d 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -266,7 +266,7 @@ let reduce c =
exception NoObligations of Id.t option
let explain_no_obligations = function
- Some ident -> str "No obligations for program " ++ str (Id.to_string ident)
+ Some ident -> str "No obligations for program " ++ Id.print ident
| None -> str "No obligations remaining"
type obligation_info =
@@ -996,7 +996,7 @@ let show_obligations_of_prg ?(msg=true) prg =
if !showed > 0 then (
decr showed;
msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
- str "of" ++ spc() ++ str (Id.to_string n) ++ str ":" ++ spc () ++
+ str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
str "." ++ fnl ())))
| Some _ -> ())
@@ -1013,14 +1013,14 @@ let show_obligations ?(msg=true) n =
let show_term n =
let prg = get_prog_err n in
let n = prg.prg_name in
- (str (Id.to_string n) ++ spc () ++ str":" ++ spc () ++
+ (Id.print n ++ spc () ++ str":" ++ spc () ++
Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
let sign = Decls.initialize_named_context_for_proof () in
- let info = str (Id.to_string n) ++ str " has type-checked" in
+ let info = Id.print n ++ str " has type-checked" in
let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3a75004b0..c432274a0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -171,7 +171,7 @@ let warning_or_error coe indsp err =
let st = match err with
| MissingProj (fi,projs) ->
let s,have = if List.length projs > 1 then "s","were" else "","was" in
- (str(Id.to_string fi) ++
+ (pr_id fi ++
strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++
strbrk " not defined.")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 28b5bace1..7144db494 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -156,7 +156,7 @@ let show_match id =
(* "Print" commands *)
let print_path_entry p =
- let dir = str (DirPath.to_string (Loadpath.logical p)) in
+ let dir = pr_dirpath (Loadpath.logical p) in
let path = str (Loadpath.physical p) in
(dir ++ str " " ++ tbrk (0, 0) ++ path)
@@ -947,7 +947,7 @@ let register_ltac local tacl =
match tactic_body with
| TacticDefinition ((loc,id), body) ->
let kn = Lib.make_kn id in
- let id_pp = str (Id.to_string id) in
+ let id_pp = pr_id id in
let () = if is_defined_tac kn then
Errors.user_err_loc (loc, "",
str "There is already an Ltac named " ++ id_pp ++ str".")
@@ -1584,7 +1584,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
let natureofid = match bdyopt with
| None -> "Hypothesis"
| Some bdy ->"Constant (let in)" in
- v 0 (str (Id.to_string id) ++ str":" ++ pr_constr typ ++ fnl() ++ fnl()
+ v 0 (pr_id id ++ str":" ++ pr_constr typ ++ fnl() ++ fnl()
++ str natureofid ++ str " of the goal context.")
with (* fallback to globals *)
| NoHyp | Not_found -> print_about ref_or_by_not
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 20:45:52 +0000