current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
type proof =
- UriManager.uri option * Cic.metasenv * Cic.term * Cic.term * Cic.attribute list
+ UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term Lazy.t * Cic.term * Cic.attribute list
(** current goal, integer index *)
type goal = int
type status = proof * goal
val goals_of_proof: proof -> goal list
+val hole: Cic.term