Removed nAuto.ml-mli

[helm.git] / matita / components / ng_tactics / nnAuto.ml

diff --git a/matita/components/ng_tactics/nnAuto.ml b/matita/components/ng_tactics/nnAuto.ml
index 344e7535c2614e2d971cd798326f9fba918a760d..96ccf0e0d5312cefb9962ab897f7c38b15d23f4d 100644 (file)
--- a/matita/components/ng_tactics/nnAuto.ml
+++ b/matita/components/ng_tactics/nnAuto.ml
@@ -1748,3 +1748,12 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
     s
 ;;
 
+let auto_tac ~params:(_,flags as params) ?trace_ref =
+  if List.mem_assoc "demod" flags then 
+    demod_tac ~params 
+  else if List.mem_assoc "paramod" flags then 
+    paramod_tac ~params 
+  else if List.mem_assoc "fast_paramod" flags then 
+    fast_eq_check_tac ~params  
+  else auto_tac ~params ?trace_ref
+;;