+
+let auto ~params:(l,_) status goal =
+ let gty = get_goalty status goal in
+ let n,h,metasenv,subst,o = status#obj in
+ let status,t = term_of_cic_term status gty (ctx_of gty) in
+ let status, l =
+ List.fold_left
+ (fun (status, l) t ->
+ let status, t = disambiguate status t None (ctx_of gty) in
+ let status, ty = typeof status (ctx_of t) t in
+ let status, t = term_of_cic_term status t (ctx_of gty) in
+ let status, ty = term_of_cic_term status ty (ctx_of ty) in
+ (status, (t,ty) :: l))
+ (status,[]) l
+ in
+ match
+ NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
+ with
+ | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
+ | (pt, metasenv, subst)::_ ->
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+;;
+
+let auto_tac ~params status =
+ distribute_tac (auto ~params) status
+;;
+