From 8db86b3a3d531c44d9a52cc5519122e5a3af3ed9 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 19 Feb 2010 11:46:35 +0000
Subject: added validation of delta_resolver (which seem to have an impact on
 typing)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12800 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/modops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'checker/modops.ml')

diff --git a/checker/modops.ml b/checker/modops.ml
index de0d6c7e9..ce2f07ab6 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -127,7 +127,9 @@ let strengthen_const env mp_from l cb resolver =
 	  
 
 let rec strengthen_mod env mp_from mp_to mb = 
-    assert(mp_from = mb.mod_mp);
+  if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
+    mb 
+  else
     match mb.mod_type with
      | SEBstruct (sign) -> 
 	 let resolve_out,sign_out = 
-- 
cgit v1.2.3