From 66314ee777ff9215dd45eb0894428537f765fc69 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 3 Feb 2005 13:14:04 +0000
Subject: [PATCH] removed uri parameter from load_proof

---
 helm/gTopLevel/gTopLevel.ml   | 6 +++---
 helm/gTopLevel/termViewer.ml  | 5 ++---
 helm/gTopLevel/termViewer.mli | 3 +--
 3 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f7d502066..de725228e 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -451,7 +451,7 @@ let qed () =
 		  Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[]) 
                 in
 		let (acic,ids_to_inner_types,ids_to_inner_sorts) =
-		  (rendering_window ())#output#load_proof uri proof
+		  (rendering_window ())#output#load_proof proof
 		in
 		  !qed_set_sensitive false ;
 		  (* let's save the theorem and register it to the getter *) 
@@ -564,7 +564,7 @@ let refresh_proof (output : TermViewer.proof_viewer) =
         (uri,
          Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]))
   in
-   ignore (output#load_proof uri currentproof)
+   ignore (output#load_proof currentproof)
  with
   e ->
  match ProofEngine.get_proof () with
@@ -864,7 +864,7 @@ let
     try
       let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures,
           ids_to_hypotheses,_,_)) =
-       ApplyTransformation.mml_of_cic_object uri obj 
+       ApplyTransformation.mml_of_cic_object obj 
       in
        window#set_title (UriManager.string_of_uri uri) ;
        window#misc#hide () ; window#show () ;
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
diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli
index 5a8ff7253..f391363eb 100644
--- a/helm/gTopLevel/termViewer.mli
+++ b/helm/gTopLevel/termViewer.mli
@@ -45,7 +45,6 @@ type mml_of_cic_sequent =
    
 
 type mml_of_cic_object =
-  UriManager.uri ->
   Cic.obj ->
   Gdome.document * 
   (Cic.annobj * 
@@ -106,7 +105,7 @@ class proof_viewer :
     (* load_proof also returns the annotated cic term and the *)
     (* ids_to_inner_types and ids_to_inner_sorts maps.        *)
     method load_proof :
-     UriManager.uri -> Cic.obj ->
+     Cic.obj ->
       Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t *
        (Cic.id, string) Hashtbl.t
 
-- 
2.39.2