(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
-type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term
+type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
(** current goal, integer index *)
type goal = int
type status = proof * goal