diff options
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 8fee8481d7..33eae08213 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -115,9 +115,11 @@ and merge_with env mtb with_decl = let _ = subst_modtype (map_msid msid (MPself msid)) mtb in () with - Assert_failure _ -> error_circular_with_module id + Failure _ -> error_circular_with_module id end; - let cst = check_subtypes env' mtb old.msb_modtype in + let cst = + try check_subtypes env' mtb old.msb_modtype + with Failure _ -> error_with_incorrect (label_of_id id) in let equiv = match old.msb_equiv with | None -> Some mp @@ -213,7 +215,10 @@ and translate_module env is_definition me = | None -> mtb1, None, Constraint.empty | Some mte -> let mtb2 = translate_modtype env mte in - mtb2, Some mtb2, check_subtypes env mtb1 mtb2 + let cst = + try check_subtypes env mtb1 mtb2 + with Failure _ -> error "not subtype" in + mtb2, Some mtb2, cst in { mod_type = mtb; mod_user_type = mod_user_type; @@ -237,7 +242,10 @@ and translate_mexpr env mexpr = match mexpr with let ftb = scrape_modtype env ftb in let farg_id, farg_b, fbody_b = destr_functor ftb in let meb,mtb = translate_mexpr env mexpr in - let cst = check_subtypes env mtb farg_b in + let cst = + try check_subtypes env mtb farg_b + with Failure _ -> + error "" in let mp = try path_of_mexpr mexpr |