Module AltErgoLib.Matching_types

type gsubst = {
sbs : Expr.t Symbols.Map.t;
sty : Ty.subst;
gen : int;
goal : bool;
s_term_orig : Expr.t list;
s_lem_orig : Expr.t;
}
type trigger_info = {
trigger : Expr.trigger;
trigger_age : int;
trigger_orig : Expr.t;
trigger_formula : Expr.t;
trigger_dep : Explanation.t;
trigger_increm_guard : Expr.t;
}
type term_info = {
term_age : int;
term_from_goal : bool;
term_from_formula : Expr.t option;
term_from_terms : Expr.t list;
}
type info = {
age : int;
lem_orig : Expr.t list;
t_orig : Expr.t list;
but : bool;
}