diff options
| author | herbelin | 2000-11-29 11:30:53 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-29 11:30:53 +0000 |
| commit | 123c3a105b69ca63c54976df74cb816437946589 (patch) | |
| tree | fa02c4de0316a6e651da62ec8540eedb178c6302 /lib/system.mli | |
| parent | 7963f0ef1839f575c4a5e3f5ac953e2709bc7a0c (diff) | |
Ajout d'un alias à add_path, rec_add_path et all_subdirs pour associer un chemin Unix à un chemin Coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1013 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/system.mli b/lib/system.mli index 18dae19151..eb07830525 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -8,11 +8,11 @@ type load_path_entry = { directory : string; root_dir : string; - relative_subdir : string } + relative_subdir : string list } type load_path = load_path_entry list -val all_subdirs : string -> load_path +val all_subdirs : unix_path:string -> string list option -> load_path val is_in_path : load_path -> string -> bool val where_in_path : load_path -> string -> load_path_entry * string |