From c2e849ca61c24253956d6b9b1e3082e58fcf08c6 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 5 Jul 2001 21:24:18 +0000
Subject: Interdiction de faire 2 variables de même nom court
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'library/declare.ml')

diff --git a/library/declare.ml b/library/declare.ml
index 81021d1be..db1ae9d98 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -70,7 +70,11 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.survive_section = false }
 
 let cache_variable (sp,(id,(d,_,_) as vd)) =
+(*
   if Nametab.exists_cci sp then
+*)
+  (* Constr raisonne sur les noms courts *)
+  if List.mem_assoc id (current_section_context ()) then
     errorlabstrm "cache_variable"
       [< pr_id (basename sp); 'sTR " already exists" >];
   begin match d with (* Fails if not well-typed *)
-- 
cgit v1.2.3