From b1eef69751a05eebdbdc9d3091e1dae3386218d0 Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 16 Aug 2002 10:00:36 +0000 Subject: Strengthenning rules for modules + No modules in sections git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/nametab.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library/nametab.ml') diff --git a/library/nametab.ml b/library/nametab.ml index bc419a237..1f8111a2c 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -106,7 +106,7 @@ let push_many vis tab dir o = | Absolute _ -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - warning "Trying to zaslonic an absolute name!"; current + warning "Trying to mask an absolute name!"; current | Nothing | Relative _ -> Relative o else current @@ -118,7 +118,7 @@ let push_many vis tab dir o = (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) (* But ours is also absolute! This is an error! *) - error "Trying to zaslonic an absolute name!" + error "Trying to mask an absolute name!" | Nothing | Relative _ -> Absolute o, dirmap in @@ -137,7 +137,7 @@ let push_one vis tab dir o = | Absolute _ -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - error "Trying to zaslonic an absolute name!" + error "Trying to mask an absolute name!" | Nothing | Relative _ -> Relative o in -- cgit v1.2.3