diff options
| author | ppedrot | 2012-12-14 15:57:08 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-14 15:57:08 +0000 |
| commit | f42dd8d8530e6227621ccd662741f1da23700304 (patch) | |
| tree | 1838306cdafaa8486ec792c1ab48b64162e027c9 /dev | |
| parent | 67f5c70a480c95cfb819fc68439781b5e5e95794 (diff) | |
Modulification of dir_path
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/top_printers.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 186ab170ee..7163f4429a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -321,7 +321,7 @@ let print_pure_constr csr = and sp_display sp = (* let dir,l = decode_kn sp in let ls = - match List.rev (List.map Id.to_string (repr_dirpath dir)) with + match List.rev (List.map Id.to_string (Dir_path.repr dir)) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l @@ -330,7 +330,7 @@ let print_pure_constr csr = and sp_con_display sp = (* let dir,l = decode_kn sp in let ls = - match List.rev (List.map Id.to_string (repr_dirpath dir)) with + match List.rev (List.map Id.to_string (Dir_path.repr dir)) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l @@ -448,10 +448,10 @@ let encode_path loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] | Some (mp,dir) -> - (repr_dirpath (dirpath_of_string (string_of_mp mp))@ - repr_dirpath dir) in + (Dir_path.repr (dirpath_of_string (string_of_mp mp))@ + Dir_path.repr dir) in Qualid (loc, make_qualid - (make_dirpath (List.rev (Id.of_string prefix::dir@suffix))) id) + (Dir_path.make (List.rev (Id.of_string prefix::dir@suffix))) id) let raw_string_of_ref loc = function | ConstRef cst -> |