big change in parsing, trying to make all functional

[helm.git] / matita / components / content_pres / termContentPres.mli

diff --git a/matita/components/content_pres/termContentPres.mli b/matita/components/content_pres/termContentPres.mli
index 41018d39000dfed3cfca57209cb49ee602435529..69cb38b998844151ab8b20a20b103c8c84606e88 100644 (file)
--- a/matita/components/content_pres/termContentPres.mli
+++ b/matita/components/content_pres/termContentPres.mli
@@ -39,13 +39,11 @@ class status :
     method set_content_pres_status: #g_status -> 'self
   end
 
-type pretty_printer_id
-
 val add_pretty_printer:
  #status as 'status ->
   NotationPt.term ->             (* level 2 pattern *)
   CicNotationParser.checked_l1_pattern ->
-   'status * pretty_printer_id
+   'status
 
   (** {2 content -> pres} *)