Module Constrintern.Interner

type t = {
  1. ref : t -> (Libnames.qualid * Constrexpr.instance_expr option) fn;
  2. fix : t -> (Names.lident * Constrexpr.fix_expr list) fn;
  3. cofix : t -> (Names.lident * Constrexpr.cofix_expr list) fn;
  4. prodn : t -> (Constrexpr.local_binder_expr list * Constrexpr.constr_expr) fn;
  5. lambdan : t -> (Constrexpr.local_binder_expr list * Constrexpr.constr_expr) fn;
  6. letin : t -> (Names.lname * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr) fn;
  7. appexpl : t -> ((Libnames.qualid * Constrexpr.instance_expr option) * Constrexpr.constr_expr list) fn;
  8. app : t -> (Constrexpr.constr_expr * (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) list) fn;
  9. proj : t -> (Constrexpr.explicit_flag * (Libnames.qualid * Constrexpr.instance_expr option) * (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) list * Constrexpr.constr_expr) fn;
  10. record : t -> (Constrexpr.constr_expr option * (Libnames.qualid * Constrexpr.constr_expr) list) fn;
  11. cases : t -> (Constr.case_style * Constrexpr.constr_expr option * Constrexpr.case_expr list * Constrexpr.branch_expr list) fn;
  12. lettuple : t -> (Names.lname list * (Names.lname option * Constrexpr.constr_expr option) * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
  13. if_ : t -> (Constrexpr.constr_expr * (Names.lname option * Constrexpr.constr_expr option) * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
  14. hole : t -> Evar_kinds.glob_evar_kind option fn;
  15. genarg : t -> GenConstr.raw fn;
  16. genargglob : t -> GenConstr.glb fn;
  17. patvar : t -> Pattern.patvar fn;
  18. evar : t -> (Glob_term.existential_name CAst.t * (Names.lident * Constrexpr.constr_expr) list) fn;
  19. sort : t -> Constrexpr.sort_expr fn;
  20. cast : t -> (Constrexpr.constr_expr * Constr.cast_kind option * Constrexpr.constr_expr) fn;
  21. notation : t -> (Constrexpr.notation_with_optional_scope option * Constrexpr.notation * Constrexpr.constr_notation_substitution) fn;
  22. generalization : t -> (Glob_term.binding_kind * Constrexpr.constr_expr) fn;
  23. prim : t -> Constrexpr.prim_token fn;
  24. delimiters : t -> (Constrexpr.delimiter_depth * string * Constrexpr.constr_expr) fn;
  25. array : t -> (Constrexpr.instance_expr option * Constrexpr.constr_expr array * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
}