First gospel/doc attribute is attached to the module if it is not preceded by a documentation one.

[n-osborne]

For example, manpage for Gospelstdlib.List is lacking the gospel type declaration and its informal documentation end up in the synopsis:

$ ocamlc -bin-annot src/stdlib/gospelstdlib.mli
$ odoc compile src/stdlib/gospelstdlib.cmti
$ odoc man-generate src/stdlib/gospelstdlib.odoc --output-dir ./
$ man Gospelstdlib.List.3o | head -n 15

List(3)                                      OCaml Library                                      List(3)

Name
       Gospelstdlib.List

Synopsis
  Module Gospelstdlib.List

       An alias for 'a list.

Documentation
       length l is the number of elements of l.

       When l contains one or more elements, hd s is the first element of l.

One could make gospel.ppx add an empty documentation attribute before the first gospel attribute (and its documentation counterpart) if it is not preceded by a documentation attribute (a real module documentation).

[n-osborne]

Unfortunately, the empty documentation attribute show up in the generated documentation