Module PrintingFlags

module Detype : sig ... end
module Extern : sig ... end
type t = {
  1. detype : Detype.t;
  2. extern : Extern.t;
}

Combined detyping and extern flags.

val make_raw : t -> t
val current : unit -> t
val current_ignore_raw : unit -> t
val print_universes : bool Stdlib.ref

The following flag is still accessed directly, but not when printing constr.

module PrintingInductiveMake (_ : sig ... end) : Goptions.RefConvertArg with type t = Names.inductive and module Set = Names.Indset_env
val set_extern_depth : int option -> unit