package rocq-runtime

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

Module Vernacentries.DefAttributesSource

Sourcetype t = {
  1. hooks : Declare.Hook.t list;
  2. scope : Locality.definition_scope;
  3. locality : bool option;
  4. poly : PolyFlags.t;
  5. program : bool;
  6. user_warns : Globnames.extended_global_reference UserWarn.with_qf option;
  7. canonical_instance : bool;
  8. typing_flags : Declarations.typing_flags option;
  9. using : Vernacexpr.section_subset_expr option;
  10. reversible : bool;
  11. clearbody : bool option;
}
Sourceval def_attributes : t Attributes.attribute