]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/content_pres/termContentPres.mli
Matitaweb:
[helm.git] / matitaB / components / content_pres / termContentPres.mli
index 9c08650c23adfa6a4ac88e17ff220d4088f610e7..f64bfcd670e356d6ccc43f91a1c784c7760784af 100644 (file)
@@ -33,6 +33,7 @@ class type g_status =
   end
 
 class virtual status :
+  string option ->
   object ('self)
     inherit NCic.status
     method content_pres_db: db
@@ -54,4 +55,5 @@ val pp_ast: #status -> NotationPt.term -> NotationPt.term
 
   (** fills a term pattern instantiating variable magics *)
 val instantiate_level2:
- #NCic.status -> NotationEnv.t -> NotationPt.term -> NotationPt.term
+ #NCic.status -> NotationEnv.t ->
+ NotationPt.term -> NotationPt.term