prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)
prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)
match CicParser.obj_of_xml prooffiletype (Some prooffile) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
match CicParser.obj_of_xml prooffiletype (Some prooffile) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
- ProofEngine.set_proof
- (Some (uri, metasenv, bo, ty)) ;
- ProofEngine.goal :=
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ refresh_proof output ;
+ set_proof_engine_goal
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
ProofEngine.set_proof
(Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
ProofEngine.set_proof
(Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
in
ProofEngine.set_proof
(Some (uri, metasenv, bo, ty)) ;
in
ProofEngine.set_proof
(Some (uri, metasenv, bo, ty)) ;