- addDebugItem "print metasenv goals and stack to stderr"
- (fun _ ->
- prerr_endline ("metasenv goals: " ^ String.concat " "
- (List.map (fun (g, _, _) -> string_of_int g)
- (MatitaScript.current ())#proofMetasenv));
- prerr_endline ("stack: " ^ Continuationals.Stack.pp
- (GrafiteTypes.get_stack (MatitaScript.current ())#grafite_status)));
- addDebugItem "Print current proof term"
- (fun _ ->
- HLog.debug
- (CicPp.ppterm
- (match
- (MatitaScript.current ())#grafite_status#proof_status
- with
- | GrafiteTypes.No_proof -> (Cic.Implicit None)
- | Incomplete_proof i ->
- let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in
- Lazy.force p
- | Proof p -> let _,_,_subst,p,_, _ = p in Lazy.force p
- | Intermediate _ -> assert false)));
- addDebugItem "Print current proof (natural language) to stderr"
- (fun _ ->
- prerr_endline
- (ApplyTransformation.txt_of_cic_object 120 []
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- (match
- (MatitaScript.current ())#grafite_status#proof_status
- with
- | GrafiteTypes.No_proof -> assert false
- | Incomplete_proof i ->
- let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in
- Cic.CurrentProof ("current (incomplete) proof",m,Lazy.force p,ty,[],attrs)
- | Proof (_,m,_subst,p,ty, attrs) ->
- Cic.CurrentProof ("current proof",m,Lazy.force p,ty,[],attrs)
- | Intermediate _ -> assert false)));