printing/Ppconstr: Cosmetics.
printing/Ppconstr.print_hunks:
        Make evaluation order explicit.
        (Do not rely anymore on ocaml evaluation order, which is unspecified.)
lib/Pp: Cosmetics.
lib/Pp.ppcmd_token:
        Extend this type with Ppcmd_open_tag and Ppcmd_close_tag.
lib/Pp.ppcmd_pp_dirs:
        Handle these tags with a straightforward translation to
        corresponding Format commands.
printing/Ppconstr.Make:
        - Functorize Ppconstr with respect to a set of tagging functions.
        - These functions are meant to introduce tags to produce semistructured
          pretty printings.

printing/Ppconstr:
        Preserve the previous behaviour of this module by instantiating Make
        with tagging functions that do nothing.
lib/Pp: Publish combinators for tags opening and closing.
Xml_datatype.gxml: New type for semi-structured documents.
Xml_parser, Xml_printer: Use it.
RichPp: New module.
        It is responsible for turning a tagged pretty-printing into
        a semi-structured document.

clib.mllib: Include RichPp as well as Xml_*.
        The migration of Xml_* from lib to clib is needed by RichPp
        depends on these modules.
Ppannotation: New.
              Define the annotations stored in semi-structured pretty-prints.

Ppconstrsig: New.
             Contains the signature of a pretty-printer for ppconstr.

Ppconstr: Export a new rich pretty-printer for constr_expr and co.
Ppvernac: Cosmetics.
Ppvernac.Make: New

 - Ppvernac is now functorized with respect to
   a Ppconstr printer.

 - Preserve previous behavior by instantiating this functor
   with Ppconstr.
Ppvernacsig: New.
  - Define the signature for a pretty-printer of vernacular commands.

Ppvernac: Use it.
Ppannotation.t: New constructor AVernac.

Ppvernac.RichPp: New rich pretty-printer.
Ppvernac: Publish new rich pretty-printer.
Ppconstr: Fix a typo in comments.
ide/{Xmlprotocol,Interface,Ide_slave}: New command "annotate".

   - Extend the protocol with a new command called "annotate".

   - By the way, relax the dependencies between the "ide" package
     and the internal packages of Coq by *not* referring to external
     type definitions inside Interface.

     Indeed, the purpose of the protocol is to act as a barrier
     between the source tree of Coq and the source tree of Coqide.
     We should enforce this property.
     (Maybe one day coqide will be extracted from the source tree
     of Coq to live its own life.)
ide/wg_ProofView: Do not refer to the {Proof} internal module, use {Interface} instead.
ide/{ide_slave.ml, interfaces}: Coerce input and output of requests between internal and external datatypes.
Xml_lexer: Handle non-breakable spaces.
lib/Xml_parser: Cosmetics.
lib/Xml_parser: Cosmetics.