Matitaweb:

[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 34e63aa649d7b5aa4784a26381d4a48110d501eb..f64bfcd670e356d6ccc43f91a1c784c7760784af 100644 (file)
--- a/matitaB/components/content_pres/termContentPres.mli
+++ b/matitaB/components/content_pres/termContentPres.mli
@@ -56,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