X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.ml;h=0f2019ad507b3a3c2d6c9a850ca537001ce3eefd;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=23d7543d3da08d19995e393b4f69596febc01426;hpb=18bd1d094e9227822ea8c0fa4f9668cd8752236f;p=helm.git

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 23d7543d3..0f2019ad5 100644
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -47,7 +47,6 @@ type mml_of_cic_sequent =
    
 
 type mml_of_cic_object =
-  UriManager.uri ->
   Cic.obj ->
   Gdome.document * 
   (Cic.annobj * 
@@ -229,12 +228,12 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
          end
     | None -> assert false (* "ERROR: No selection!!!" *)
 
-  method load_proof uri currentproof =
+  method load_proof currentproof =
     let mml,
          (acic,
            (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
             ids_to_hypotheses,ids_to_inner_sorts,ids_to_inner_types)) =
-      mml_of_cic_object uri currentproof
+      mml_of_cic_object currentproof
     in
     current_infos <-
       Some