status,[]
| GrafiteAst.Print (_,"proofterm") ->
let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
- prerr_endline (Auto.pp_proofterm p);
+ prerr_endline (Auto.pp_proofterm (Lazy.force p));
status,[]
| GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Qed loc ->
(GrafiteTypes.Command_error
"Proof not completed! metasenv is not empty!");
let name = UriManager.name_of_uri uri in
- let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ let obj = Cic.Constant (name,Some (Lazy.force bo),ty,[],attrs) in
let status, lemmas = add_obj uri obj status in
{status with
GrafiteTypes.proof_status = GrafiteTypes.No_proof},
"\nPlease use a variant."));
end;
let _subst = [] in
- let initial_proof = (Some uri, metasenv', _subst, bo, ty, attrs) in
+ let initial_proof = (Some uri, metasenv', _subst, lazy bo, ty, attrs) in
let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
{ status with GrafiteTypes.proof_status =
GrafiteTypes.Incomplete_proof