X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=3c5bf8441555a33c98bd54d273616c4b018be067;hb=ff5659b6ee47292a33c84b0889b5d66d729397f6;hp=58b7de9f34c2a9f02d94b39cc0ac589e5d0ecc8d;hpb=5bc000d9a2e8e41db58d610f3221270add686888;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 58b7de9f3..3c5bf8441 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -149,6 +149,17 @@ let _ =
             (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.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 "ask record choice"
       (fun _ ->
         HLog.debug (string_of_int