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
| GrafiteAst.Tactic (_(*loc*), Some tac, punct) ->
let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
let status = eval_tactical status (tactic_of_ast' tac) in
- (* CALL auto on every goal, easy way of testing it
+ (* CALL auto on every goal, easy way of testing it
let auto =
GrafiteAst.AutoBatch
(loc, ([],["depth","2";"timeout","1";"type","1"])) in
(try
let auto = apply_tactic ~disambiguate_tactic ("",0,auto) in
let _ = eval_tactical status (tactic_of_ast' auto) in
- print_endline "GOOD"; ()
- with ProofEngineTypes.Fail _ -> print_endline "BAD" | _ -> ());
- *)
+ print_endline "GOOD"; ()
+ with ProofEngineTypes.Fail _ -> print_endline "BAD" | _ -> ());*)
eval_tactical status
(punctuation_tactical_of_ast (text,prefix_len,punct)),[]
| GrafiteAst.Tactic (_, None, punct) ->