Keeping track of locations of disambiguated ids and symbols.

[helm.git] / matitaB / components / content_pres / termContentPres.mli

diff --git a/matitaB/components/content_pres/termContentPres.mli b/matitaB/components/content_pres/termContentPres.mli
index 9c08650c23adfa6a4ac88e17ff220d4088f610e7..cd7d1ee3f9f454a6eb4eab75d2b0df2eab9a6800 100644 (file)
--- a/matitaB/components/content_pres/termContentPres.mli
+++ b/matitaB/components/content_pres/termContentPres.mli
@@ -54,4 +54,4 @@ 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 -> Stdpp.location -> NotationPt.term -> NotationPt.term