t',[],Cic.Implicit (Some `Hole)
(** tactic failure *)
-exception Fail of string
+exception Fail of string Lazy.t
(**
calls the opaque tactic on the status, restoring the original
(** 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
+