From 890696ca0c475a8e169882c49256356cd96b447f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Apr 2002 12:49:25 +0000
Subject: Interdiction de nommer une constante comme une variable de section
 (plus simple que d'afficher en nom long...)

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

diff --git a/library/declare.ml b/library/declare.ml
index 6c715bfe28..a67260d01b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -123,6 +123,9 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.survive_section = false }
 
 let cache_constant (sp,(cdt,stre)) =
+  (if Idmap.mem (basename sp) !vartab then
+    errorlabstrm "cache_constant" 
+      (pr_id (basename sp) ++ str " already exists"));
   (if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
     errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
@@ -204,6 +207,9 @@ let inductive_names sp mie =
   in names
 
 let check_exists_inductive (sp,_) =
+  (if Idmap.mem (basename sp) !vartab then
+    errorlabstrm "cache_inductive" 
+      (pr_id (basename sp) ++ str " already exists"));
   if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
     errorlabstrm "cache_inductive" (pr_id id ++ str " already exists")
-- 
cgit v1.2.3