(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
-type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
+type proof =
+ UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
(** current goal, integer index *)
type goal = int
type status = proof * goal
(** @param goal
* @param goal's metasenv
* @return initial proof status for the given goal *)
-val initial_status: Cic.term -> Cic.metasenv -> status
+val initial_status: Cic.term -> Cic.metasenv -> Cic.attribute list -> status
(**
a tactic: make a transition from one status to another one or, usually,
val goals_of_proof: proof -> goal list
+val hole: Cic.term