let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
res,metasenv @ newmetasenv,arguments,lastmeta
+let lookup_type metasenv context hyp =
+ 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 (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
+ | _ :: tail -> aux (succ p) tail
+ | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal")
+ in
+ aux 1 context