val empty : tval make :
max_t_depth:int ->
Matching_types.info AltErgoLib.Expr.Map.t ->
Expr.t list AltErgoLib.Expr.Map.t AltErgoLib.Symbols.Map.t ->
Matching_types.trigger_info list ->
tval add_term : Matching_types.term_info -> Expr.t -> t -> tval add_triggers :
Util.matching_env ->
t ->
(Expr.t * int * Explanation.t) AltErgoLib.Expr.Map.t ->
tval terms_info :
t ->
Matching_types.info AltErgoLib.Expr.Map.t
* Expr.t list AltErgoLib.Expr.Map.t AltErgoLib.Symbols.Map.tval query :
Util.matching_env ->
t ->
theory ->
(Matching_types.trigger_info * Matching_types.gsubst list) list