+ addDebugItem "Print current proof term"
+ (fun _ ->
+ HLog.debug
+ (CicPp.ppterm
+ (match
+ (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
+ with
+ | GrafiteTypes.No_proof -> (Cic.Implicit None)
+ | Incomplete_proof i -> let _,_,p,_ = i.GrafiteTypes.proof in p
+ | Proof p -> let _,_,p,_ = p in p
+ | Intermediate _ -> assert false)));
+ addDebugItem "Print current proof (natural language) to stderr"
+ (fun _ ->
+ prerr_endline
+ (ObjPp.obj_to_string 120
+ (match
+ (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
+ with
+ | GrafiteTypes.No_proof -> assert false
+ | Incomplete_proof i ->
+ let _,m,p,ty = i.GrafiteTypes.proof in
+ Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],[])
+ | Proof (_,m,p,ty) ->
+ Cic.CurrentProof ("current proof",m,p,ty,[],[])
+ | Intermediate _ -> assert false)));