doc corrections

Fix inacurracies noticed while reimplementing the module and macro system.

pkgs/racket-doc/scribblings/reference/eval-model.scrbl

@@ -791,9 +791,10 @@ binding is not included in the @tech{lexical information} for the
 module body. If a new variable definition has a counterpart in the old
 declaration, it effectively assigns to the old variable.
 
-If a module is @tech{instantiate}d in any @tech{phase}s before it is
+If a module is @tech{instantiate}d in the current namespace's
-redeclared, each redeclaration of the module is immediately
+@tech{base phase} before the module is redeclared, the redeclaration
-@tech{instantiate}d in the same @tech{phase}s.
+of the module is immediately @tech{instantiate}d in that
+@tech{phase}.
 
 If the current @tech{inspector} does not manage a module's declaration
 inspector (see @secref["modprotect"]), then the module cannot be

pkgs/racket-doc/scribblings/reference/namespaces.scrbl

@@ -22,7 +22,8 @@ otherwise.}
 @defproc[(make-empty-namespace) namespace?]{
 
 Creates a new @tech{namespace} that is empty, and whose @tech{module
-registry} contains no mappings. The namespace's @tech{base phase} is
+registry} contains only mappings for some internal, predefined modules,
+such as @racket['#%kernel]. The namespace's @tech{base phase} is
 the same as the @tech{base phase} of the @tech{current
 namespace}. Attach modules from an existing namespace to the new one
 with @racket[namespace-attach-module].
@@ -207,9 +208,9 @@ corresponding to the @tech{namespace}'s @tech{base phase}.}
 Performs the import corresponding to @racket[quoted-raw-require-spec]
 in the top-level environment of the current namespace, like a
 top-level @racket[#%require]. The @racket[quoted-raw-require-spec]
-argument must be a datum that corresponds to a quoted
+argument must be either a datum that corresponds to a quoted
 @racket[_raw-require-spec] for @racket[#%require], which includes
-module paths.
+module paths, or it can be a @tech{resolved module path}.
 
 Module paths in @racket[quoted-raw-require-spec] are resolved with respect
 to @racket[current-load-relative-directory] or
@@ -249,7 +250,7 @@ undefined.}
 
 
 @defproc[(namespace-attach-module [src-namespace namespace?]
-                                  [modname module-path?]
+                                  [modname (or module-path? resolved-module-path?)]
                                   [dest-namespace namespace? (current-namespace)])
          void?]{
 
@@ -330,7 +331,7 @@ Changes the inspector for the instance of the module referenced by
 that it is controlled by the current code inspector. The given
 @racket[inspector] must currently control the invocation of the module
 in @racket[namespace]'s @tech{module registry}, otherwise the
-@exnraise[exn:fail:contract]. See also @secref["modprotect"].}
+inspector is not changed. See also @secref["modprotect"].}
 
 
 @defproc[(namespace-module-registry [namespace namespace?])

pkgs/racket-doc/scribblings/reference/stx-taints.scrbl

@@ -88,7 +88,7 @@ the transformer's input. The @tech{rearm}ing process
  @item{If the result has no @racket['taint-mode] property value, but
           its datum is a pair, and if the syntax object corresponding
           to the @racket[car] of the pair is an identifier bound to
-          @racket[begin], @racket[module], or
+          @racket[begin], @racket[begin-for-syntax], or
           @racket[#%plain-module-begin], then dye packs are propagated
           as if the syntax object had the @racket['transparent]
           property value.}

pkgs/racket-doc/scribblings/reference/stx-trans.scrbl

@@ -969,7 +969,7 @@ and different result procedures use distinct scopes.
 
 Produces a procedure that behaves like the result of
 @racket[make-syntax-introducer], but using a set of @tech{scopes} from
-@racket[ext-stx] and with a default action of @racket['remove].
+@racket[ext-stx] and with a default action of @racket['add].
 
 @itemlist[
 
@@ -1029,8 +1029,9 @@ level as reported by @racket[syntax-local-phase-level].}
 @defproc[(syntax-local-module-required-identifiers
           [mod-path (or/c module-path? #f)]
           [phase-level (or/c exact-integer? #f #t)])
-         (listof (cons/c (or/c exact-integer? #f)
+         (or/c (listof (cons/c (or/c exact-integer? #f)
-                         (listof identifier?)))]{
+                               (listof identifier?)))
+               #f)]{
 
 Can be called only while
 @racket[syntax-local-transforming-module-provides?] returns
@@ -1042,7 +1043,9 @@ identifiers.  Each list of identifiers includes all bindings imported
 @racket[mod-path], or all modules if @racket[mod-path] is
 @racket[#f]. The association list includes all identifiers imported
 with a @racket[phase-level] shift, or all shifts if
-@racket[phase-level] is @racket[#t].
+@racket[phase-level] is @racket[#t]. If @racket[phase-level] is
+not @racket[#t], the result can be @racket[#f] if no identifiers
+are exported at that phase.
 
 When an identifier is renamed on import, the result association list
 includes the identifier by its internal name. Use

pkgs/racket-doc/scribblings/reference/syntax.scrbl

@@ -236,7 +236,8 @@ A @racket[module*] form in which the enclosing module's bindings are visible
 can define or import bindings that @tech{shadow} the enclosing module's bindings.
 
 The evaluation of a @racket[module] form does not evaluate the
-expressions in the body of the module. Evaluation merely declares a
+expressions in the body of the module (except sometimes for redeclarations;
+see @secref["module-redeclare"]). Evaluation merely declares a
 module, whose full name depends both on @racket[id] or
 @racket[(current-module-declare-name)].
 
@@ -682,7 +683,7 @@ corresponds to the default @tech{module name resolver}.
  @racket[current-directory]).  Regardless of the current platform,
  @racket[rel-string] is always parsed as a Unix-format relative path:
  @litchar{/} is the path delimiter (multiple adjacent @litchar{/}s are
- treated as a single delimiter), @litchar{..} accesses the parent
+ not allowed), @litchar{..} accesses the parent
  directory, and @litchar{.} accesses the current directory. The path
  cannot be empty or contain a leading or trailing slash, path elements
  before than the last one cannot include a file suffix (i.e., a
@@ -1215,7 +1216,8 @@ composable, and not extensible. Also, sub-form names like
 @racketidfont{for-syntax} and @racketidfont{lib} are recognized
 symbolically, instead of via bindings. Although not formalized in the
 grammar above, a @racketidfont{just-meta} form cannot appear within a
-@racketidfont{just-meta} form.
+@racketidfont{just-meta} form, but it can appear under @racketidfont{for-meta},
+ @racketidfont{for-syntax}, @racketidfont{for-template}, or @racketidfont{for-label}.
 
 Each @racket[raw-require-spec] corresponds to the obvious
 @racket[_require-spec], but the @racketidfont{rename} sub-form has the