diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-29 16:20:11 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-29 20:30:43 +0200 |
commit | 0932339dbf44e4ef2b04426f7b4ac6d74b2f4f1f (patch) | |
tree | 90057464a1a39f4d1de1af4193be6e6ebe998072 /kernel/mod_typing.ml | |
parent | 95cd90c7e552b4362201abf671c68c5fbe950547 (diff) |
Remove unused Failure catch
Unused since dc57718e98289b5d71a0a942d6a063d441dc6a54 as far as I can
tell.
Diffstat (limited to 'kernel/mod_typing.ml')
-rw-r--r-- | kernel/mod_typing.ml | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index d2b41aae9..8568bf14b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -166,16 +166,10 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = let mb_mp1 = lookup_module mp1 env in let mtb_mp1 = module_type_of_module mb_mp1 in let cst = match old.mod_expr with - | Abstract -> - begin - try - let mtb_old = module_type_of_module old in - let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in - Univ.ContextSet.add_constraints chk_cst old.mod_constraints - with Failure _ -> - (* TODO: where can a Failure come from ??? *) - error_incorrect_with_constraint lab - end + | Abstract -> + let mtb_old = module_type_of_module old in + let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in + Univ.ContextSet.add_constraints chk_cst old.mod_constraints | Algebraic (NoFunctor (MEident(mp'))) -> check_modpath_equiv env' mp1 mp'; old.mod_constraints |