From b6cbbb30f6272f93e8d0c3de4da4165ad079109d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 Oct 2003 08:46:23 +0000
Subject: Protection contre les noms de lemmes existant deja

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4607 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index a7cac8ac68..fb95bdc345 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -630,12 +630,12 @@ let start_proof_com sopt kind (bl,t) hook =
   let id = match sopt with
     | Some id ->
         (* We check existence here: it's a bit late at Qed time *)
-        if Nametab.exists_cci (Lib.make_path id) then
+        if is_global id then
           errorlabstrm "start_proof" (pr_id id ++ str " already exists");
         id
     | None ->
-	next_ident_away (id_of_string "Unnamed_thm")
-	  (Pfedit.get_all_proof_names ())
+	next_global_ident_away false (id_of_string "Unnamed_thm")
+ 	  (Pfedit.get_all_proof_names ())
   in
   let env = Global.env () in
   let c = interp_type Evd.empty env (generalize_rawconstr t bl) in
-- 
cgit v1.2.3