(** constraint: the returned value will always be constructed by Cic.Name **)
type mk_fresh_name_type =
Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+
+let goals_of_proof (_,metasenv,_,_) = List.map (fun (g,_,_) -> g) metasenv
+