package rocq-runtime
Module Ppconstr.CompactedDeclSource
Source
type t = | LocalAssum of (Environ.var_status option * Names.Id.t EConstr.binder_annot) list * EConstr.types| LocalDef of (Environ.var_status option * Names.Id.t EConstr.binder_annot) list * EConstr.constr * EConstr.types
Source
val to_tuple :
t ->
Names.Id.t EConstr.binder_annot list * EConstr.constr option * EConstr.types