Declaration (rocq-runtime.Context.Compacted.Declaration)

type ('constr, 'types, 'r) pt =

| LocalAssum of (Names.Id.t, 'r) pbinder_annot list * 'types

| LocalDef of (Names.Id.t, 'r) pbinder_annot list * 'constr * 'types

val map_constr : ('c -> 'c) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt

val of_named_decl : ('c, 't, 'r) Named.Declaration.pt -> ('c, 't, 'r) pt

val to_named_context : ('c, 't, 'r) pt -> ('c, 't, 'r) Named.pt