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} *)
(** fills a term pattern instantiating variable magics *)
val instantiate_level2:
- NotationEnv.t -> NotationPt.term ->
- NotationPt.term
+ #NCic.status -> NotationEnv.t -> NotationPt.term -> NotationPt.term