diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-24 15:07:17 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-24 15:07:17 +0000 |
| commit | dc57718e98289b5d71a0a942d6a063d441dc6a54 (patch) | |
| tree | 3e8136faef19ef7d1e8280177de78c56582d1f35 /kernel/mod_typing.ml | |
| parent | c155e42cdd1dd70b9e20243a6dc599ec653aef7a (diff) | |
modifications des messages d'erreurs renvoyés lors de la comparaison
de deux signatures de modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9531 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 785778235..824d2e4eb 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 |