X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.mli;h=4d0bb909b97ee65ae9d1f7a744e32435d67c37e3;hb=42680d47c033d751738fd0f84af7b45b2a91a5b8;hp=cd7d1ee3f9f454a6eb4eab75d2b0df2eab9a6800;hpb=3ffb8f47701d127211a095d3b9f64d363760430f;p=helm.git

diff --git a/matitaB/components/content_pres/termContentPres.mli b/matitaB/components/content_pres/termContentPres.mli
index cd7d1ee3f..4d0bb909b 100644
--- a/matitaB/components/content_pres/termContentPres.mli
+++ b/matitaB/components/content_pres/termContentPres.mli
@@ -54,4 +54,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