- 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