X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtermViewer.mli;h=f391363ebdf48730caac1dcbb9b0138a06589322;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=71ab63bc0e0ca9c861bc84d16b037115957fafb5;hpb=f36273550bc0538ea194cf0dee32ec608a6790f7;p=helm.git

diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli
index 71ab63bc0..f391363eb 100644
--- a/helm/gTopLevel/termViewer.mli
+++ b/helm/gTopLevel/termViewer.mli
@@ -36,17 +36,24 @@
 type mml_of_cic_sequent =
  Cic.metasenv ->
  int * Cic.context * Cic.term ->
- Gdome.document *
+ Gdome.document * 
+ (Cic.annconjecture *
   ((Cic.id, Cic.term) Hashtbl.t *
    (Cic.id, Cic.id option) Hashtbl.t *
-   (string, Cic.hypothesis) Hashtbl.t)
+   (string, Cic.hypothesis) Hashtbl.t *
+   (Cic.id, string) Hashtbl.t))
+   
 
 type mml_of_cic_object =
-  explode_all:bool ->
-  UriManager.uri ->
-  Cic.annobj ->
-  (string, string) Hashtbl.t ->
-  (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
+  Cic.obj ->
+  Gdome.document * 
+  (Cic.annobj * 
+   ((Cic.id, Cic.term) Hashtbl.t * 
+    (Cic.id, Cic.id option) Hashtbl.t *
+    (Cic.id, Cic.conjecture) Hashtbl.t * 
+    (Cic.id, Cic.hypothesis) Hashtbl.t *
+    (Cic.id, string) Hashtbl.t *   
+    (Cic.id, Cic2acic.anntypes) Hashtbl.t))
 
 (** A widget to render sequents **)
 
@@ -98,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