package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Extern.Records`Source

Sourcetype t

Sourceval make_raw : t -> t

Sourceval current : unit -> t

Sourceval current_ignore_raw : unit -> t

Sourceval use_record_syntax : t -> Names.inductive -> bool

Tells whether record syntax should be used for some record. If the inductive is not a record, the result is meaningless.