Granting wish #2249 (checking existing lemma name also when in a section).

Simplified in passing generation of names for the "Goal" command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12910 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 9 insertions, 3 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 9c11cd991..c8f5c6258 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -111,13 +111,17 @@ let sections_are_opened () =
 
 let cwd () = fst !path_prefix
 
+let cwd_except_section () =
+  Libnames.pop_dirpath_n (sections_depth ()) (cwd ())
+
 let current_dirpath sec =
   Libnames.drop_dirpath_prefix (library_dp ())
-    (if sec then cwd ()
-      else Libnames.pop_dirpath_n (sections_depth ()) (cwd ()))
+    (if sec then cwd () else cwd_except_section ())
 
 let make_path id = Libnames.make_path (cwd ()) id
 
+let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id
+
 let path_of_include () =
   let dir = Names.repr_dirpath (cwd ()) in
   let new_dir = List.tl dir in
diff --git a/library/lib.mli b/library/lib.mli
index 32d1c0009..13c9baf65 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -79,8 +79,10 @@ val contents_after : Libnames.object_name option -> library_segment
 
 (* User-side names *)
 val cwd : unit -> Names.dir_path
-val current_dirpath : bool -> Names.dir_path
+val cwd_except_section : unit -> Names.dir_path
+val current_dirpath : bool -> Names.dir_path (* false = except sections *)
 val make_path : Names.identifier -> Libnames.full_path
+val make_path_except_section : Names.identifier -> Libnames.full_path
 val path_of_include : unit -> Libnames.full_path
 
 (* Kernel-side names *)