diff options
author | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
commit | 7f076db2a924377e9de3f9a6d838b8c44ed2e16d (patch) | |
tree | e075c526532a227c83d951c9dff8c944ea0c4d15 /kernel/modops.ml | |
parent | 2a14f39fdfa80b021227396b22e38ed7c35356df (diff) | |
parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) |
Merge commit 'upstream/8.1+dfsg' into 8.1
Diffstat (limited to 'kernel/modops.ml')
-rw-r--r-- | kernel/modops.ml | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 5cc2a84d..8bab3c9d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 9138 2006-09-14 15:20:45Z jforest $ i*) +(*i $Id: modops.ml 9558 2007-01-30 14:58:42Z soubiran $ i*) (*i*) open Util @@ -20,6 +20,8 @@ open Entries open Mod_subst (*i*) +exception Circularity of string + let error_existing_label l = error ("The label "^string_of_label l^" is already declared") @@ -83,6 +85,13 @@ let error_local_context lo = let error_circular_with_module l = error ("The construction \"with Module "^(string_of_id l)^":=...\" is about to create\na circular module type. Their resolution is not implemented yet.\nIf you really need that feature, please report.") +let error_circularity_in_subtyping l l1 l2 = + error ("An occurrence of "^l^" creates a circularity\n during the subtyping verification between "^l1^" and "^l2^".") + +let error_no_such_label_sub l l1 l2 = + error (l1^" is not a subtype of "^l2^".\nThe field "^(string_of_label l)^" is missing (or invisible) in "^l1^".") + + let rec scrape_modtype env = function | MTBident kn -> scrape_modtype env (lookup_modtype kn env) | mtb -> mtb @@ -134,12 +143,12 @@ let rec subst_modtype sub = function M to M' I must substitute M' for X in "Module N := X". *) | MTBident ln -> MTBident (subst_kn sub ln) | MTBfunsig (arg_id, arg_b, body_b) -> - if occur_mbid arg_id sub then failwith "capture"; + if occur_mbid arg_id sub then raise (Circularity (string_of_mbid arg_id)); MTBfunsig (arg_id, subst_modtype sub arg_b, subst_modtype sub body_b) | MTBsig (sid1, msb) -> - if occur_msid sid1 sub then failwith "capture"; + if occur_msid sid1 sub then raise (Circularity (string_of_msid sid1)); MTBsig (sid1, subst_signature sub msb) and subst_signature sub sign = |