diff options
| author | letouzey | 2013-02-19 20:27:51 +0000 |
|---|---|---|
| committer | letouzey | 2013-02-19 20:27:51 +0000 |
| commit | 248728628f5da946f96c22ba0a0e7e9b33019382 (patch) | |
| tree | 905dbbafa65dd7bf02823318326be2ca389f833f /dev | |
| parent | 3889c9a9e7d017ef2eea647d8c17d153a0b90083 (diff) | |
Dir_path --> DirPath
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 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 9386c82de0..0dc09f9baf 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -322,7 +322,7 @@ let print_pure_constr csr = and sp_display sp = (* let dir,l = decode_kn sp in let ls = - match List.rev_map Id.to_string (Dir_path.repr dir) with + match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l @@ -331,7 +331,7 @@ let print_pure_constr csr = and sp_con_display sp = (* let dir,l = decode_kn sp in let ls = - match List.rev_map Id.to_string (Dir_path.repr dir) with + match List.rev_map Id.to_string (DirPath.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l @@ -449,10 +449,10 @@ let encode_path loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] | Some (mp,dir) -> - (Dir_path.repr (dirpath_of_string (string_of_mp mp))@ - Dir_path.repr dir) in + (DirPath.repr (dirpath_of_string (string_of_mp mp))@ + DirPath.repr dir) in Qualid (loc, make_qualid - (Dir_path.make (List.rev (Id.of_string prefix::dir@suffix))) id) + (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) let raw_string_of_ref loc = function | ConstRef cst -> |