NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
with
| [] -> raise (Error (lazy "no proof found",None))
- | (pt, metasenv, subst)::_ ->
+ | (pt, _, metasenv, subst)::_ ->
let status = status#set_obj (n,h,metasenv,subst,o) in
instantiate status goal (mk_cic_term (ctx_of gty) pt)
;;