- [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
- GA.Auto (floc,["paramodulation","";"timeout",string_of_int !paramod_timeout])),
- Some (GA.Dot(floc))));
- GA.Executable(floc,GA.Tactical(floc, GA.Try(floc,
- GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc))))
+ [GA.Executable(floc,GA.Tactic(floc, Some (
+ if ueq_case then
+ GA.Auto (floc,["paramodulation","";
+ "timeout",string_of_int !paramod_timeout])
+ else
+ GA.Auto (floc,["depth",string_of_int !depth])
+ ),
+ GA.Dot(floc)));
+ GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
+ GA.Assumption floc)), GA.Dot(floc)))