let paramodulation = bool "paramodulation" params in
let full = bool "full" params in
let superposition = bool "superposition" params in
- let what = string "what" params in
- let other = string "other" params in
+ let target = string "target" params in
+ let table = string "table" params in
let subterms_only = bool "subterms_only" params in
- let demodulate = bool "demodulate" params in
+ let demod_table = string "demod_table" params in
(* the real tactic *)
let auto_tac dbd (proof, goal) =
let normal_auto () =
match superposition with
| true ->
ProofEngineTypes.mk_tactic
- (Saturation.superposition_tac ~what ~other ~subterms_only ~demodulate)
+ (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table)
| _ -> ProofEngineTypes.mk_tactic (auto_tac dbd)
;;