From a0cd5003d9cdb8a2a060e47837a566348d215ac9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 Oct 2003 12:43:42 +0000
Subject: Bug introduit dans start_proof par le commit precedent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4621 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index fb95bdc345..df3dc78d5a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -630,7 +630,7 @@ 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 is_global id then
+        if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
           errorlabstrm "start_proof" (pr_id id ++ str " already exists");
         id
     | None ->
-- 
cgit v1.2.3