From fac949450909b5ef17078f220ae809cf54ae3f08 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 20 Aug 2013 08:22:42 +0000 Subject: Safe_typing code refactoring - No more modinfo sub-record in the safe_environment record, this was a syntactic pain. senv.modinfo.modpath --> senv.modpath senv.modinfo.variant --> senv.modvariant senv.modinfo.resolver --> senv.modresolver senv.modinfo.resolver_of_param --> senv.paramresolver senv.modinfo.label : removed (can be inferred from modpath) - No more systematic chaining of safe_environment ('old' field). Instead, earlier safe_environment is stored in the modvariant field when necessary (STRUCT and SIG case). - Improved sharing between end_module and end_modtype - More qualified names instead of open, better comments, ... - Some user errors are now checked earlier elsewhere (see for instance vernac_end_segment), so we can turn these errors into asserts. The user error about higher-order include is now algebraic. - Highlight the idea of a state monad in Safe_typing : type 'a safe_transformer = safe_environment -> 'a * safe_environment More systematic code in Global, thanks to 'globalize' function. - Declaremods : less informations stored in openmod_info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16708 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/modops.mli | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) (limited to 'kernel/modops.mli') diff --git a/kernel/modops.mli b/kernel/modops.mli index c0943233b..ea92c45ea 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -87,15 +87,13 @@ type module_typing_error = | NoSuchLabel of Label.t | IncompatibleLabels of Label.t * Label.t | SignatureExpected of struct_expr_body - | NoModuleToEnd - | NoModuleTypeToEnd | NotAModule of string | NotAModuleType of string | NotAConstant of Label.t | IncorrectWithConstraint of Label.t | GenerativeModuleExpected of Label.t - | NonEmptyLocalContect of Label.t option | LabelMissing of Label.t * string + | HigherOrderInclude exception ModuleTypingError of module_typing_error @@ -115,10 +113,6 @@ val error_no_such_label : Label.t -> '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_module : string -> 'a val error_not_a_constant : Label.t -> 'a @@ -127,6 +121,6 @@ val error_incorrect_with_constraint : Label.t -> 'a val error_generative_module_expected : Label.t -> 'a -val error_non_empty_local_context : Label.t option -> 'a - val error_no_such_label_sub : Label.t->string->'a + +val error_higher_order_include : unit -> 'a -- cgit v1.2.3