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 | 55ce117e8083477593cf1ff2e51a3641c7973830 (patch) | |
| tree | a82defb4105f175c71b0d13cae42831ce608c4d6 /kernel/modops.ml | |
| parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) | |
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
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 = |