diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index bd1151544e..e9e1d67eb4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -20,7 +20,6 @@ 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") @@ -82,11 +81,6 @@ let error_local_context lo = error ("The local context of the component "^ (string_of_label l)^" is not empty") -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^".") @@ -142,12 +136,10 @@ 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 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 raise (Circularity (string_of_msid sid1)); MTBsig (sid1, subst_signature sub msb) and subst_signature sub sign = |