X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnAuto.ml;h=7a33d6266da45052fc2a16328d60f8dcbf5ce5b8;hb=89fc31fc5cc01e8860cf67a8e096c24125370d31;hp=6f49f7d36575b4c9d21cf9e66a768728d1bcda0d;hpb=a14adba81c00c9dcb9996d7af39e4803214606f1;p=helm.git

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 6f49f7d36..7a33d6266 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1709,7 +1709,7 @@ let auto_tac ~params =
 ;;
 
 (* ========================= dispatching of auto/auto_paramod ============ *)
-let auto_tac ~params:(_,flags as params) =
+let auto_tac ~params:(_,flags as params) ?trace_ref =
   if List.mem_assoc "paramodulation" flags then 
     auto_paramod_tac ~params 
   else if List.mem_assoc "demod" flags then 
@@ -1719,7 +1719,7 @@ let auto_tac ~params:(_,flags as params) =
   else if List.mem_assoc "fast_paramod" flags then 
     NnAuto.fast_eq_check_tac ~params  
   else if List.mem_assoc "slir" flags then 
-    NnAuto.auto_tac ~params  
+    NnAuto.auto_tac ~params ?trace_ref
   else 
     auto_tac ~params
 ;;