From 0c2dd4a32538ebda7c964c249f158054b6cc2e1a Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 5 Mar 2011 16:42:38 +0000 Subject: Starting being more explicit on the reasons why module subtyping fails. Note: I'm unsure about some subtyping error case apparently involving aliases of inductive types (middle of Subtyping.check_inductive); I bound it to some NotEqualInductiveAliases error, but this has to be checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13885 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/modops.mli | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) (limited to 'kernel/modops.mli') diff --git a/kernel/modops.mli b/kernel/modops.mli index f34fa88c4..cf8d62043 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -51,6 +51,27 @@ val subst_modtype_and_resolver : module_type_body -> module_path -> env -> val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body +(** Errors *) + +type signature_mismatch_error = + | InductiveFieldExpected of mutual_inductive_body + | DefinitionFieldExpected + | ModuleFieldExpected + | ModuleTypeFieldExpected + | NotConvertibleInductiveField of identifier + | NotConvertibleConstructorField of identifier + | NotConvertibleBodyField + | NotConvertibleTypeField + | NotSameConstructorNamesField + | NotSameInductiveNameInBlockField + | FiniteInductiveFieldExpected of bool + | InductiveNumbersFieldExpected of int + | InductiveParamsNumberField of int + | RecordFieldExpected of bool + | RecordProjectionsExpected of name list + | NotEqualInductiveAliases + | NoTypeConstraintExpected + val error_existing_label : label -> 'a val error_declaration_not_path : module_struct_entry -> 'a @@ -64,7 +85,8 @@ val error_incompatible_modtypes : val error_not_equal : module_path -> module_path -> 'a -val error_not_match : label -> structure_field_body -> 'a +val error_not_match : + label -> structure_field_body -> signature_mismatch_error -> 'a val error_incompatible_labels : label -> label -> 'a -- cgit v1.2.3