matitaGui: some missing cases during disambiguation now treated

[helm.git] / components / content_pres / objPp.mli

diff --git a/components/content_pres/objPp.mli b/components/content_pres/objPp.mli
index 9367661ec4c782ad2baca66b9579ef6c74f13aff..de320bf14d9fb85f19bef203c590368924fa506a 100644 (file)
--- a/components/content_pres/objPp.mli
+++ b/components/content_pres/objPp.mli
@@ -24,4 +24,5 @@
  *)
 
 (* columns, rendering style, name prefix, object *)
-val obj_to_string: int -> GrafiteAst.style -> string -> Cic.obj -> string
+val obj_to_string: 
+   int -> GrafiteAst.presentation_style -> string -> Cic.obj -> string