CSC: tentative definition of the ocaml structure that represents

[helm.git] / helm / gTopLevel / termViewer.ml

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 5291c3587bee7dc440cd42bfbfb0a43310fa8aa6..a54db659d60c8bab686eb021ae20ecc9807a611d 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -210,14 +210,9 @@ class proof_viewer obj =
          Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
            let time1 = Sys.time () in
            let content = 
-              Cic2content.acic2content 
-                 (ref 0) ~name:(Some "prova") ~ids_to_inner_sorts ~ids_to_inner_types bo in
-           let content2pres =
-             (Content2pres.proof2pres 
-               (function p -> 
-                 (Cexpr2pres.cexpr2pres_charcount 
-                    (Content_expressions.acic2cexpr ids_to_inner_sorts p)))) in
-           let pres = content2pres content in
+              Cic2content.annobj2content 
+                ~ids_to_inner_sorts ~ids_to_inner_types acic in
+           let pres = Content2pres.content2pres ~ids_to_inner_sorts content in
            let time2 = Sys.time () in
            (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *)
            let xmlpres = Mpresentation.print_mpres pres in