PrintingFlags (p.rocq-runtime.9.2.0.doc.rocq-runtime.pretyping.PrintingFlags)

Sourcemodule Detype : sig ... end

Sourcemodule Extern : sig ... end

Sourcetype t = {

}

Combined detyping and extern flags.

Sourceval make_raw : t -> t

Sourceval current : unit -> t

Sourceval current_ignore_raw : unit -> t

Sourceval print_universes : bool 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

Sourceval set_extern_depth : int option -> unit