X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FtermContentPres.mli;h=9c08650c23adfa6a4ac88e17ff220d4088f610e7;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=41018d39000dfed3cfca57209cb49ee602435529;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/matita/components/content_pres/termContentPres.mli b/matita/components/content_pres/termContentPres.mli
index 41018d390..9c08650c2 100644
--- a/matita/components/content_pres/termContentPres.mli
+++ b/matita/components/content_pres/termContentPres.mli
@@ -32,20 +32,19 @@ class type g_status =
     method content_pres_db: db
   end
 
-class status :
+class virtual status :
   object ('self)
+    inherit NCic.status
     method content_pres_db: db
     method set_content_pres_db: db -> 'self
     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} *)
 
@@ -55,5 +54,4 @@ val pp_ast: #status -> NotationPt.term -> NotationPt.term
 
   (** fills a term pattern instantiating variable magics *)
 val instantiate_level2:
-  NotationEnv.t -> NotationPt.term ->
-    NotationPt.term
+ #NCic.status -> NotationEnv.t -> NotationPt.term -> NotationPt.term