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

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