(status, (t,ty) :: l))
(status,[]) l
in
- let pt, metasenv, subst =
- Paramod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
- in
- let status = status#set_obj (n,h,metasenv,subst,o) in
- instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+ 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 =