aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_typing.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-29 16:20:11 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-29 20:30:43 +0200
commit0932339dbf44e4ef2b04426f7b4ac6d74b2f4f1f (patch)
tree90057464a1a39f4d1de1af4193be6e6ebe998072 /kernel/mod_typing.ml
parent95cd90c7e552b4362201abf671c68c5fbe950547 (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.ml14
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