5.2 Module Declaration

Introduction
"We assume that the static-context processing and dynamic-context
processing described in [5 Modules and Prologs] are applied to all library
modules before the normalization, static context processing, and dynamic
context processing of the main module."
    I don't think the inference rules make that assumption. However, they
    probably should. See technical comments.

Notation

"a module's URI"
    The proper terminology appears to be "a module's target namespace".

Core Grammar
[5 (Core)] ModuleDecl ::= ...
    This production is never used. Might as well delete it.

SCP + DCP

SCP / rule 1 / premise 1
"declare namespace NCName = URILiteral ; PrologDeclList =>stat statEnv"
    Append "with PrologDeclList1".
    Prepend "statEnvDefault |-"

DCP / rule 1 / premise 1
"(declare namespace NCName = URILiteral PrologDeclList) =>dyn dynEnv"
    Delete parentheses.
    Prepend "dynEnvDefault |-"
(leftover from last year, comment #146)

SCP / rule 1 / premise 2
DCP / rule 1 / premise 1
DCP / rule 1 / premise 2
"... namespace NCName = URILiteral PrologDeclList"
    Insert semicolon between "URILiteral" and "PrologDeclList".
(leftover from last year, comment #146, #147)

SCP / rule 1 / premise 2
DCP / rule 1 / premise 2
"module namespace NCName = URILiteral ; PrologDeclList"
    This is not a judgment.
(leftover from last year, comment #147)