diff options
Diffstat (limited to 'toplevel/ide_slave.ml')
-rw-r--r-- | toplevel/ide_slave.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 98ba3e792..fcec3a128 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -231,11 +231,11 @@ let inloadpath dir = Library.is_in_load_paths (CUnix.physical_path_of_string dir) let status () = - (** We remove the initial part of the current [Dir_path.t] + (** We remove the initial part of the current [DirPath.t] (usually Top in an interactive session, cf "coqtop -top"), and display the other parts (opened sections and modules) *) let path = - let l = Names.Dir_path.repr (Lib.cwd ()) in + let l = Names.DirPath.repr (Lib.cwd ()) in List.rev_map Names.Id.to_string l in let proof = |