;;
(* ========================= dispatching of auto/auto_paramod ============ *)
-let auto_tac ~params:(_,flags as params) =
+let auto_tac ~params:(_,flags as params) ?trace_ref =
if List.mem_assoc "paramodulation" flags then
auto_paramod_tac ~params
else if List.mem_assoc "demod" flags then
else if List.mem_assoc "fast_paramod" flags then
NnAuto.fast_eq_check_tac ~params
else if List.mem_assoc "slir" flags then
- NnAuto.auto_tac ~params
+ NnAuto.auto_tac ~params ?trace_ref
else
auto_tac ~params
;;