X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoTactic.ml;h=63dc8631dbc8b4b564fded81c72ea44fcffe204c;hb=41e76668e9389ce17e41747026e533f907a0311c;hp=1ba1dd912495f63801c7ffbf90b0d785e93e883e;hpb=679f6296c9a979213425104fa606809d9f1e3bad;p=helm.git

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 1ba1dd912..63dc8631d 100644
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -328,10 +328,10 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
   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 () = 
@@ -378,7 +378,7 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
   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)
 ;;