From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Sat, 18 Aug 2007 20:34:57 +0000
Subject: Imported Upstream version 8.1.pl1+dfsg

---
 kernel/mod_typing.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 352a1e46..70de3034 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mod_typing.ml 9558 2007-01-30 14:58:42Z soubiran $ i*)
+(*i $Id: mod_typing.ml 9980 2007-07-12 13:32:37Z soubiran $ i*)
 
 open Util
 open Names
@@ -131,8 +131,12 @@ and merge_with env mtb with_decl =
 	    let equiv = 
  	      match old.msb_equiv with
 		| None -> Some mp
-		| Some mp' -> 
-		    check_modpath_equiv env' mp mp';
+		| Some mp' ->
+		    begin
+		      try 
+			check_modpath_equiv env' mp mp'
+		      with Not_equiv_path -> error_not_equal mp mp
+		    end;
 		    Some mp
 	    in
 	    let msb =
-- 
cgit v1.2.3