+ let params' =
+ if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
+ ("paramodulation","1")::params
+ else params
+ in
+ if params = params' then
+ Tactics.auto ~dbd ~params:(univ, params) ~automation_cache
+ else
+ Tacticals.first
+ [Tactics.auto ~dbd ~params:(univ, params) ~automation_cache ;
+ Tactics.auto ~dbd ~params:(univ, params') ~automation_cache]
+ | `Term just -> Tactics.apply just
+ | `SolveWith term ->
+ Tactics.demodulate ~automation_cache ~dbd
+ ~params:(Some [term],
+ ["all","1";"steps","1"; "use_context","false"])
+ | `Proof ->
+ Tacticals.id_tac