diff options
| author | Matej Košík | 2017-05-29 11:02:06 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-06-10 10:33:53 +0200 |
| commit | b6feaafc7602917a8ef86fb8adc9651ff765e710 (patch) | |
| tree | 5a033488c31040009adb725f20e8bd0a5dd31bc5 /dev | |
| parent | 102d7418e399de646b069924277e4baea1badaca (diff) | |
Remove (useless) aliases from the API.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a1b3c81b9a..6ae5125f6d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -37,7 +37,7 @@ let pp x = Pp.pp_with !Topfmt.std_ft x let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) (* name printers *) -let ppid id = pp (pr_id id) +let ppid id = pp (Id.print id) let pplab l = pp (pr_lab l) let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) let ppdir dir = pp (pr_dirpath dir) @@ -79,12 +79,12 @@ let ppbigint n = pp (str (Bigint.to_string n));; let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Int.Set.elements l)) -let ppidset l = pp (prset pr_id (Id.Set.elements l)) +let ppidset l = pp (prset Id.print (Id.Set.elements l)) let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" let pridmap pr l = - let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in + let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) let ppidmap pr l = pp (pridmap pr l) @@ -95,10 +95,10 @@ let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ Termops.print_constr (EConstr.of_constr c) ++ str">") ++ (if id = id0 then mt () - else spc () ++ str "<canonical: " ++ pr_id id ++ str ">")))) + else spc () ++ str "<canonical: " ++ Id.print id ++ str ">")))) -let prididmap = pridmap (fun _ -> pr_id) -let ppididmap = ppidmap (fun _ -> pr_id) +let prididmap = pridmap (fun _ -> Id.print) +let ppididmap = ppidmap (fun _ -> Id.print) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") @@ -132,15 +132,15 @@ let safe_pr_global = function int i ++ str ")") | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") - | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")") + | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")") let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x let ppconst (sp,j) = - pp (str"#" ++ pr_kn sp ++ str"=" ++ pr_lconstr j.uj_val) + pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val) let ppvar ((id,a)) = - pp (str"#" ++ pr_id id ++ str":" ++ pr_lconstr a) + pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a) let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) @@ -538,21 +538,21 @@ let encode_path ?loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] | Some (mp,dir) -> - (DirPath.repr (dirpath_of_string (string_of_mp mp))@ + (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in Qualid (Loc.tag ?loc @@ make_qualid (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) let raw_string_of_ref ?loc _ = function | ConstRef cst -> - let (mp,dir,id) = repr_con cst in + let (mp,dir,id) = Constant.repr3 cst in encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id) | IndRef (kn,i) -> - let (mp,dir,id) = repr_mind kn in + let (mp,dir,id) = MutInd.repr3 kn in encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> - let (mp,dir,id) = repr_mind kn in + let (mp,dir,id) = MutInd.repr3 kn in encode_path ?loc "CSTR" (Some (mp,dir)) [Label.to_id id;Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) @@ -561,14 +561,14 @@ let raw_string_of_ref ?loc _ = function let short_string_of_ref ?loc _ = function | VarRef id -> Ident (Loc.tag ?loc id) - | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_con cst))) - | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_mind kn))) + | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst))) + | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn))) | IndRef (kn,i) -> - encode_path ?loc "IND" None [Label.to_id (pi3 (repr_mind kn))] + encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> encode_path ?loc "CSTR" None - [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)] + [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) (* Anticipate that printers can be used from ocamldebug and that |
