diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-05 16:42:42 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-05 16:42:42 +0000 |
commit | 19d89158f4e0e4be5998f2ff9b64e90270977a32 (patch) | |
tree | 99dd65665fdbfe64be95cb870da5e710ec4d8c8e /kernel/modops.mli | |
parent | 0c2dd4a32538ebda7c964c249f158054b6cc2e1a (diff) |
Moving printing of module typing errors upwards to himsg.ml so as to
be able to call term printers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13886 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/modops.mli')
-rw-r--r-- | kernel/modops.mli | 49 |
1 files changed, 26 insertions, 23 deletions
diff --git a/kernel/modops.mli b/kernel/modops.mli index cf8d62043..35be04665 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -72,53 +72,56 @@ type signature_mismatch_error = | NotEqualInductiveAliases | NoTypeConstraintExpected -val error_existing_label : label -> 'a +type module_typing_error = + | SignatureMismatch of label * structure_field_body * signature_mismatch_error + | LabelAlreadyDeclared of label + | ApplicationToNotPath of module_struct_entry + | NotAFunctor of struct_expr_body + | IncompatibleModuleTypes of module_type_body * module_type_body + | NotEqualModulePaths of module_path * module_path + | NoSuchLabel of label + | IncompatibleLabels of label * label + | SignatureExpected of struct_expr_body + | NoModuleToEnd + | NoModuleTypeToEnd + | NotAModule of string + | NotAModuleType of string + | NotAConstant of label + | IncorrectWithConstraint of label + | GenerativeModuleExpected of label + | NonEmptyLocalContect of label option + | LabelMissing of label * string + +exception ModuleTypingError of module_typing_error -val error_declaration_not_path : module_struct_entry -> 'a +val error_existing_label : label -> 'a val error_application_to_not_path : module_struct_entry -> 'a -val error_not_a_functor : module_struct_entry -> 'a - val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a -val error_not_equal : module_path -> module_path -> 'a - -val error_not_match : +val error_signature_mismatch : label -> structure_field_body -> signature_mismatch_error -> 'a val error_incompatible_labels : label -> label -> 'a val error_no_such_label : label -> 'a -val error_result_must_be_signature : unit -> 'a - val error_signature_expected : struct_expr_body -> 'a val error_no_module_to_end : unit -> 'a val error_no_modtype_to_end : unit -> 'a -val error_not_a_modtype_loc : loc -> string -> 'a - -val error_not_a_module_loc : loc -> string -> 'a - -val error_not_a_module_or_modtype_loc : loc -> string -> 'a - val error_not_a_module : string -> 'a val error_not_a_constant : label -> 'a -val error_with_incorrect : label -> 'a +val error_incorrect_with_constraint : label -> 'a -val error_a_generative_module_expected : label -> 'a +val error_generative_module_expected : label -> 'a -val error_local_context : label option -> 'a +val error_non_empty_local_context : label option -> 'a val error_no_such_label_sub : label->string->'a - -val error_with_in_module : unit -> 'a - -val error_application_to_module_type : unit -> 'a - |