X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=f9916befc851b48a2eeca70d6aa7d476fc819740;hb=a3ee89dab26307ce1cedc8041ede995a97d51446;hp=a0d8eba48a6b555718c45625968ccc6ddc451666;hpb=a9c8d96d47a5895c99bca2fe93decf464bca62c3;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index a0d8eba48..f9916befc 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -553,3 +553,15 @@ let assert_tac seqs status =
           [merge_tac])
      ) status
 ;;
+
+let auto ~params status goal =
+  let gty = get_goalty status goal in
+  let n,h,metasenv,subst,o = status.pstatus in
+  let status,t = term_of_cic_term status gty (ctx_of gty) in
+    Paramod.nparamod metasenv subst (ctx_of gty) t;      
+    status
+;;
+
+let auto_tac ~params status =
+  distribute_tac (auto ~params) status
+;;