Constrintern.Interner
type 'a fn = Environ.env -> intern_env -> bool -> (ltac_sign * Genintern.ntnvar_status Names.Id.Map.t) -> ?loc:Loc.t -> 'a -> Glob_term.glob_constr
type t = {
ref : t -> (Libnames.qualid * Constrexpr.instance_expr option) fn;
fix : t -> (Names.lident * Constrexpr.fix_expr list) fn;
cofix : t -> (Names.lident * Constrexpr.cofix_expr list) fn;
prodn : t -> (Constrexpr.local_binder_expr list * Constrexpr.constr_expr) fn;
lambdan : t -> (Constrexpr.local_binder_expr list * Constrexpr.constr_expr) fn;
letin : t -> (Names.lname * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr) fn;
appexpl : t -> ((Libnames.qualid * Constrexpr.instance_expr option) * Constrexpr.constr_expr list) fn;
app : t -> (Constrexpr.constr_expr * (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) list) fn;
proj : t -> (Constrexpr.explicit_flag * (Libnames.qualid * Constrexpr.instance_expr option) * (Constrexpr.constr_expr * Constrexpr.explicitation CAst.t option) list * Constrexpr.constr_expr) fn;
record : t -> (Libnames.qualid * Constrexpr.constr_expr) list fn;
cases : t -> (Constr.case_style * Constrexpr.constr_expr option * Constrexpr.case_expr list * Constrexpr.branch_expr list) fn;
lettuple : t -> (Names.lname list * (Names.lname option * Constrexpr.constr_expr option) * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
if_ : t -> (Constrexpr.constr_expr * (Names.lname option * Constrexpr.constr_expr option) * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
hole : t -> Evar_kinds.glob_evar_kind option fn;
genarg : t -> Genarg.raw_generic_argument fn;
genargglob : t -> Genarg.glob_generic_argument fn;
patvar : t -> Pattern.patvar fn;
evar : t -> (Glob_term.existential_name CAst.t * (Names.lident * Constrexpr.constr_expr) list) fn;
sort : t -> Constrexpr.sort_expr fn;
cast : t -> (Constrexpr.constr_expr * Constr.cast_kind option * Constrexpr.constr_expr) fn;
notation : t -> (Constrexpr.notation_with_optional_scope option * Constrexpr.notation * Constrexpr.constr_notation_substitution) fn;
generalization : t -> (Glob_term.binding_kind * Constrexpr.constr_expr) fn;
prim : t -> Constrexpr.prim_token fn;
delimiters : t -> (Constrexpr.delimiter_depth * string * Constrexpr.constr_expr) fn;
array : t -> (Constrexpr.instance_expr option * Constrexpr.constr_expr array * Constrexpr.constr_expr * Constrexpr.constr_expr) fn;
}
val eval : t -> Constrexpr.constr_expr_r fn