Constr (rocq-runtime.Procq.Constr)

val constr : Constrexpr.constr_expr Entry.t

val constr_eoi : Constrexpr.constr_expr Entry.t

val lconstr : Constrexpr.constr_expr Entry.t

val binder_constr : Constrexpr.constr_expr Entry.t

val term : Constrexpr.constr_expr Entry.t

val ident : Names.Id.t Entry.t

val global : Libnames.qualid Entry.t

val universe_name : Constrexpr.sort_name_expr Entry.t

val sort : Constrexpr.sort_expr Entry.t

val sort_family : Sorts.family Entry.t

val pattern : Constrexpr.cases_pattern_expr Entry.t

val constr_pattern : Constrexpr.constr_expr Entry.t

val cpattern : Constrexpr.constr_expr Entry.t

val closed_binder : Constrexpr.local_binder_expr list Entry.t

val binder : Constrexpr.local_binder_expr list Entry.t

val binders : Constrexpr.local_binder_expr list Entry.t

val open_binders : Constrexpr.local_binder_expr list Entry.t

val one_open_binder : Constrexpr.kinded_cases_pattern_expr Entry.t

val one_closed_binder : Constrexpr.kinded_cases_pattern_expr Entry.t

val binders_fixannot : (Constrexpr.local_binder_expr list * Constrexpr.fixpoint_order_expr option) Entry.t

val typeclass_constraint : (Names.lname * bool * Constrexpr.constr_expr) Entry.t

val record_declaration : Constrexpr.constr_expr Entry.t

val arg : (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) Entry.t

val type_cstr : Constrexpr.constr_expr Entry.t