diff options
| author | filliatr | 1999-12-08 15:15:47 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-08 15:15:47 +0000 |
| commit | c4dccc430e10b784e65b5bf3330c55d658d2883d (patch) | |
| tree | 42afd0f7ff5f3c2079f65597fe15f46a1b830203 /library/lib.mli | |
| parent | b3e6d156fbc13ae6d79075265fc20f8912c520da (diff) | |
deplacement de Discharge dans toplevel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/lib.mli b/library/lib.mli index 56bbcd59cf..3d87abe4db 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -34,7 +34,7 @@ val contents_after : section_path option -> library_segment (*s Opening and closing a section. *) val open_section : string -> section_path -val close_section : string -> unit +val close_section : string -> section_path * library_segment val make_path : identifier -> path_kind -> section_path val cwd : unit -> string list |