X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.mli;h=34e63aa649d7b5aa4784a26381d4a48110d501eb;hb=ae6757199708cc32166961debb52d48114c0eb74;hp=cd7d1ee3f9f454a6eb4eab75d2b0df2eab9a6800;hpb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git diff --git a/matitaB/components/content_pres/termContentPres.mli b/matitaB/components/content_pres/termContentPres.mli index cd7d1ee3f..34e63aa64 100644 --- a/matitaB/components/content_pres/termContentPres.mli +++ b/matitaB/components/content_pres/termContentPres.mli @@ -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,6 @@ val pp_ast: #status -> NotationPt.term -> NotationPt.term (** fills a term pattern instantiating variable magics *) val instantiate_level2: - #NCic.status -> NotationEnv.t -> Stdpp.location -> NotationPt.term -> NotationPt.term + #NCic.status -> NotationEnv.t -> + Stdpp.location * string option * string option -> + NotationPt.term -> NotationPt.term