-let fwd_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
- ~hyp ~dbd =
- let find_type metasenv context =
- let rec aux p = function
- | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t
- | Some (Cic.Name name, Cic.Def (_, Some t)) :: _ when name = hyp -> p, t
- | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
- p, fst (TC.type_of_aux' metasenv tail u U.empty_ugraph)
- | _ :: tail -> aux (succ p) tail
- | [] -> error fail_msg1
- in
- aux 1 context
- in