diff options
-rwxr-xr-x | library/nametab.ml | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index c0812c2d2..e50a0e6b9 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -117,12 +117,18 @@ struct (this, ModIdmap.add modid ptab' dirmap) | [] -> match current with - | Absolute (n,_) -> - (* 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 ("Cannot mask an absolute name \"" - ^ U.to_string n ^ "\"!") + | Absolute (uname',o') -> + if o'=o then begin + assert (uname=uname'); + current, dirmap + (* we are putting the same thing for the second time :) *) + end + else + (* 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 ("Cannot mask the absolute name \"" + ^ U.to_string uname' ^ "\"!") | Nothing | Relative _ -> Absolute (uname,o), dirmap @@ -139,7 +145,7 @@ let rec push_exactly uname o level (current,dirmap) = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - warning ("Trying to mask an absolute name \"" + warning ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"); current | Nothing |