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

3 files changed, 15 insertions, 12 deletions

diff --git a/library/lib.ml b/library/lib.ml
index 9c11cd991e..c8f5c62585 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 32d1c0009b..13c9baf65c 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 *)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 247fbbc0a5..f80fbf201d 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -185,19 +185,16 @@ let save_named opacity =
 
 let default_thm_id = id_of_string "Unnamed_thm"
 
-let compute_proof_name = function
+let compute_proof_name locality = function
   | Some (loc,id) ->
       (* We check existence here: it's a bit late at Qed time *)
-      if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+      if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
+	 locality=Global && Nametab.exists_cci (Lib.make_path_except_section id)
+      then
         user_err_loc (loc,"",pr_id id ++ str " already exists.");
       id
   | None ->
-      let rec next avoid id =
-        let id = next_global_ident_away id avoid in
-        if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id
-        else id
-      in
-      next (Pfedit.get_all_proof_names ()) default_thm_id
+      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) 
 
 let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
   match body with
@@ -318,7 +315,7 @@ let start_proof_com kind thms hook =
     let t', imps' = interp_type_evars_impls ~evdref env t in
     Sign.iter_rel_context (check_evars env Evd.empty !evdref) ctx;
     let len = List.length ctx in
-      (compute_proof_name sopt,
+      (compute_proof_name (fst kind) sopt,
       (nf_isevar !evdref (it_mkProd_or_LetIn t' ctx),
        (len, imps @ lift_implicits len imps'),
        guard)))