Invocation of paramod

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 5c5bb471b7d3c30c1f19ca8712d859eaa56fd098..ad9c155ca597ef0ae50f8c5ebb96a861b0d1c545 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -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