diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_typing.ml | 16 | ||||
| -rw-r--r-- | kernel/modops.ml | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 1 |
3 files changed, 14 insertions, 7 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 diff --git a/kernel/modops.ml b/kernel/modops.ml index 7459dcad8d..569580bfb1 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -125,12 +125,12 @@ let rec check_modpath_equiv env mp1 mp2 = let rec subst_modtype sub = function | MTBident ln -> MTBident (subst_kn sub ln) | MTBfunsig (arg_id, arg_b, body_b) -> - assert (not (occur_mbid arg_id sub)); + if occur_mbid arg_id sub then failwith "capture"; MTBfunsig (arg_id, subst_modtype sub arg_b, subst_modtype sub body_b) | MTBsig (sid1, msb) -> - assert (not (occur_msid sid1 sub)); + if occur_msid sid1 sub then failwith "capture"; MTBsig (sid1, subst_signature sub msb) and subst_signature sub sign = diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 6b0931a9e3..50aeaf3473 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -244,4 +244,3 @@ and check_modtypes cst env mtb1 mtb2 equiv = let check_subtypes env sup super = check_modtypes Constraint.empty env sup super false - |