+
+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
+;;