Use of standard OCaml syntax

[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 69cb38b998844151ab8b20a20b103c8c84606e88..06dfa70e09c9dbe2ca38f126de21e4bb5dfb57e4 100644 (file)
--- a/matita/components/content_pres/termContentPres.mli
+++ b/matita/components/content_pres/termContentPres.mli
@@ -32,15 +32,16 @@ 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
 
 val add_pretty_printer:
- #status as 'status ->
+ (#status as 'status) ->
   NotationPt.term ->             (* level 2 pattern *)
   CicNotationParser.checked_l1_pattern ->
    'status
@@ -53,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