(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
-type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
+type proof =
+ 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
let newmeta_idx = aux 0 metasenv in
let _subst = [] in
let proof =
- None, (newmeta_idx, [], ty) :: metasenv, _subst, Cic.Meta (newmeta_idx, []), ty, attrs
+ None, (newmeta_idx, [], ty) :: metasenv, _subst,
+ lazy (Cic.Meta (newmeta_idx, [])), ty, attrs
in
(proof, newmeta_idx)