Record
module Ast : sig ... end
val definition_structure :
Constrexpr.cumul_univ_decl_expr option ->
Vernacexpr.inductive_kind ->
template:bool option ->
cumulative:bool ->
poly:bool ->
primitive_proj:bool ->
Declarations.recursivity_kind ->
Ast.t list ->
Names.GlobRef.t list
module Data : sig ... end
module Record_decl : sig ... end
A record is an inductive mie
with extra metadata in records
val interp_structure :
Constrexpr.cumul_univ_decl_expr option ->
Vernacexpr.inductive_kind ->
template:bool option ->
cumulative:bool ->
poly:bool ->
primitive_proj:bool ->
Declarations.recursivity_kind ->
Ast.t list ->
Record_decl.t
Ast.t list at the constr level
val declare_existing_class : Names.GlobRef.t -> unit
module Internal : sig ... end