From 354712eb845676e1e49632bc176015bb8a770e59 Mon Sep 17 00:00:00 2001 From: coq Date: Thu, 10 Oct 2002 08:58:52 +0000 Subject: Nametab permet de definir le meme truc la deuxieme fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3111 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/nametab.ml | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) (limited to 'library/nametab.ml') 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 -- cgit v1.2.3