diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 6 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 2 | ||||
| -rw-r--r-- | printing/printer.ml | 4 | ||||
| -rw-r--r-- | printing/printmod.ml | 2 |
4 files changed, 7 insertions, 7 deletions
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 |