Inductive FileSectionOrderingT :=
    (** The section must be the first in the file. *)
    FSO_MustBeFirst
  | (** The section must be the last in the file. *)
    FSO_MustBeLast
  | (** The section can appear anywhere in the file. *)
    FSO_AnyOrder
  .
