package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `PrintingFlags`Source

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