ocaml 3.09 transition

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

diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli
index 8fa37e53193f2e19ed4f56cf10c696bc106a8159..f391363ebdf48730caac1dcbb9b0138a06589322 100644 (file)
--- 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 **)
 
@@ -73,7 +80,6 @@ val sequent_viewer :
   ?vadjustment:GData.adjustment ->
   ?font_size:int ->
   ?log_verbosity:int ->
-  ?border_width:int ->
   ?width:int ->
   ?height:int ->
   ?packing:(GObj.widget -> unit) ->
@@ -99,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
 
@@ -111,7 +117,6 @@ val proof_viewer :
   ?vadjustment:GData.adjustment ->
   ?font_size:int ->
   ?log_verbosity:int ->
-  ?border_width:int ->
   ?width:int ->
   ?height:int ->
   ?packing:(GObj.widget -> unit) ->