X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=b8814d4d8a7b133c3b87f4c0a0a73c80ed55c637;hb=5c10d402b5de7233bc83d7f685b274832e383212;hp=163e6db6d7e6ba7e1478f3a3d9ec72fbf1803dd2;hpb=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index 163e6db6d..b8814d4d8 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -60,3 +60,12 @@ val disambiguate_nterm :
  NCic.context -> NCic.metasenv -> NCic.substitution ->
  CicNotationPt.term Disambiguate.disambiguator_input ->
    NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term
+
+type pattern = 
+  CicNotationPt.term Disambiguate.disambiguator_input option * 
+  (string * NCic.term) list * NCic.term option
+
+val disambiguate_npattern:
+  GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
+    
+