aboutsummaryrefslogtreecommitdiff
path: root/checker/modops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/modops.ml')
-rw-r--r--checker/modops.ml9
1 files changed, 1 insertions, 8 deletions
diff --git a/checker/modops.ml b/checker/modops.ml
index 3d07135d1d..de0d6c7e96 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -127,10 +127,7 @@ 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 mp_in_delta mb.mod_mp mb.mod_delta then
- mb
- else*)
+ assert(mp_from = mb.mod_mp);
match mb.mod_type with
| SEBstruct (sign) ->
let resolve_out,sign_out =
@@ -180,10 +177,6 @@ and strengthen_sig env mp_from sign mp_to resolver =
resolve_out,item::rest'
let strengthen env mtb mp =
-(* if mp_in_delta mtb.typ_mp mtb.typ_delta then
- (* in this case mtb has already been strengthened*)
- mtb
- else*)
match mtb.typ_expr with
| SEBstruct (sign) ->
let resolve_out,sign_out =