| _::tl -> find_hyp (n+1) tl
in
let arg,gty = find_hyp 1 context in
- let last_hyp_name_of_status (proof,goal) =
- let curi, metasenv, pbo, pty = proof in
- let metano,context,gty = CicUtil.lookup_meta goal metasenv in
- match context with
- (Some (Cic.Name s,_))::_ -> s
- | _ -> assert false
- in
- let dummy = "dummy" in
+ let dummy = "dummy" in
Some arg,false,
(fun ~term typ ->
Tacticals.seq