-let auto ~params:(l,_) 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
- 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
- let rdb = status.estatus in
- let pt, metasenv, subst =
- Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
- in
- let status = { status with pstatus = 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
-;;