]> matita.cs.unibo.it Git - helm.git/commitdiff
Invocation of paramod
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 18 Jan 2010 09:59:04 +0000 (09:59 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 18 Jan 2010 09:59:04 +0000 (09:59 +0000)
helm/software/components/ng_tactics/nAuto.ml

index 5c5bb471b7d3c30c1f19ca8712d859eaa56fd098..ad9c155ca597ef0ae50f8c5ebb96a861b0d1c545 100644 (file)
@@ -1709,6 +1709,8 @@ let auto_tac ~params =
 let auto_tac ~params:(_,flags as params) =
   if List.mem_assoc "paramodulation" flags then 
     auto_paramod_tac ~params 
+  else if List.mem_assoc "paramod" flags then 
+    NnAuto.paramod_tac ~params 
   else if List.mem_assoc "fast_paramod" flags then 
     NnAuto.fast_eq_check_tac ~params  
   else if List.mem_assoc "slir" flags then