diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-16 10:00:36 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-08-16 10:00:36 +0000 |
| commit | b1eef69751a05eebdbdc9d3091e1dae3386218d0 (patch) | |
| tree | e7c3c7b3657f1d15e6931e71f77d1da4114d2b2c /library/nametab.ml | |
| parent | a1858ecd34bd7946dab7e7fbf2413036f78f7109 (diff) | |
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
Diffstat (limited to 'library/nametab.ml')
| -rwxr-xr-x | library/nametab.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |