aboutsummaryrefslogtreecommitdiff
path: root/kernel/mod_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_typing.ml')
-rw-r--r--kernel/mod_typing.ml15
1 files changed, 5 insertions, 10 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 785778235f..824d2e4eb5 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -120,10 +120,10 @@ and merge_with env mtb with_decl =
we check that there is no msid bound in mtb *)
begin
try
- let _ = subst_modtype (map_msid msid (MPself msid)) mtb in
+ let _ = subst_modtype (map_msid msid (MPself msid)) mtb in
()
with
- Failure _ -> error_circular_with_module id
+ Circularity _ -> error_circular_with_module id
end;
let cst =
try check_subtypes env' mtb old.msb_modtype
@@ -247,9 +247,7 @@ and translate_module env is_definition me =
| None -> mtb1, None, Constraint.empty
| Some mte ->
let mtb2 = translate_modtype env mte in
- let cst =
- try check_subtypes env mtb1 mtb2
- with Failure _ -> error "not subtype" in
+ let cst = check_subtypes env mtb1 mtb2 in
mtb2, Some mtb2, cst
in
{ mod_type = mtb;
@@ -274,10 +272,7 @@ 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 =
- try check_subtypes env mtb farg_b
- with Failure _ ->
- error "" in
+ let cst = check_subtypes env mtb farg_b in
let mp =
try
path_of_mexpr mexpr
@@ -290,7 +285,7 @@ and translate_mexpr env mexpr = match mexpr with
(* This is the place where the functor formal parameter is
substituted by the given argument to compute the type of the
functor application. *)
- subst_modtype
+ subst_modtype
(map_mbid farg_id mp (Some resolve)) fbody_b
| MEstruct (msid,structure) ->
let structure,signature = translate_entry_list env msid true structure in