From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 18 Jan 2010 09:59:04 +0000 (+0000)
Subject: Invocation of paramod
X-Git-Tag: make_still_working~3113
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=88efee4c688d660d2205c5933d302770acb5b407;p=helm.git

Invocation of paramod
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 5c5bb471b..ad9c155ca 100644
--- 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