aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/modops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/modops.ml')
-rw-r--r--checker/modops.ml4
1 files changed, 3 insertions, 1 deletions
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 =