package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module PrintingFlagsSource

Sourcemodule Detype : sig ... end
Sourcemodule Extern : sig ... end
Sourcetype t = {
  1. detype : Detype.t;
  2. extern : Extern.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.

Sourceval set_extern_depth : int option -> unit