X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.mli;h=f64bfcd670e356d6ccc43f91a1c784c7760784af;hb=ccf5878f2a2ec7f952f140e162391708a740517b;hp=4d0bb909b97ee65ae9d1f7a744e32435d67c37e3;hpb=42680d47c033d751738fd0f84af7b45b2a91a5b8;p=helm.git diff --git a/matitaB/components/content_pres/termContentPres.mli b/matitaB/components/content_pres/termContentPres.mli index 4d0bb909b..f64bfcd67 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 @@ -55,5 +56,4 @@ val pp_ast: #status -> NotationPt.term -> NotationPt.term (** fills a term pattern instantiating variable magics *) val instantiate_level2: #NCic.status -> NotationEnv.t -> - Stdpp.location * string option * string option -> NotationPt.term -> NotationPt.term