diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 14:30:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 14:30:01 +0000 |
| commit | f6d8fc17dc9474e4d043cf709d672d9259599354 (patch) | |
| tree | 3e05dce982c2bebb63f432064136d927a227e0c7 /library/lib.mli | |
| parent | 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea (diff) | |
Nicer code concerning dirpaths and modpath around Lib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/library/lib.mli b/library/lib.mli index 1362fabf8..fa3bd3f48 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -81,12 +81,10 @@ val cwd_except_section : unit -> Names.DirPath.t val current_dirpath : bool -> Names.DirPath.t (* false = except sections *) val make_path : Names.Id.t -> Libnames.full_path val make_path_except_section : Names.Id.t -> Libnames.full_path -val path_of_include : unit -> Libnames.full_path (** Kernel-side names *) -val current_prefix : unit -> Names.module_path * Names.DirPath.t +val current_mp : unit -> Names.module_path val make_kn : Names.Id.t -> Names.kernel_name -val make_con : Names.Id.t -> Names.constant (** Are we inside an opened section *) val sections_are_opened : unit -> bool |