- sync with the new ApplyTransformation API

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

diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli
index 71ab63bc0e0ca9c861bc84d16b037115957fafb5..5a8ff7253bb48d1601eb55f1fa5f4fcb2c38440b 100644 (file)
--- a/helm/gTopLevel/termViewer.mli
+++ b/helm/gTopLevel/termViewer.mli
@@ -36,17 +36,25 @@
 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 **)