X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.mli;h=f13fc418cd381ae6f20d36fe96fbb0f53887b1cf;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=7a2e2dda877280596bbefae2bd39cbaa673eda98;hpb=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index 7a2e2dda8..f13fc418c 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -37,13 +37,13 @@ type lazy_tactic =
 val disambiguate_tactic:
  LexiconEngine.status ref ->
  Cic.context ->
- Cic.metasenv ->
+ Cic.metasenv -> int option ->
  tactic Disambiguate.disambiguator_input ->
   Cic.metasenv * lazy_tactic
 
 val disambiguate_command: 
  LexiconEngine.status ->
- baseuri:string option ->
+ ?baseuri:string ->
  Cic.metasenv ->
  ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
   LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
@@ -52,5 +52,25 @@ val disambiguate_macro:
  LexiconEngine.status ref ->
  Cic.metasenv ->
  Cic.context ->
- (CicNotationPt.term GrafiteAst.macro) Disambiguate.disambiguator_input ->
-  Cic.metasenv * Cic.term GrafiteAst.macro
+ ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->
+  Cic.metasenv * (Cic.term,Cic.lazy_term) GrafiteAst.macro
+
+val disambiguate_nterm :
+ NCic.term option -> LexiconEngine.status ->
+ NCic.context -> NCic.metasenv -> NCic.substitution ->
+ CicNotationPt.term Disambiguate.disambiguator_input ->
+   NCic.metasenv * NCic.substitution * LexiconEngine.status * NCic.term
+
+val disambiguate_nobj :
+ LexiconEngine.status -> ?baseuri:string ->
+ (CicNotationPt.term CicNotationPt.obj) Disambiguate.disambiguator_input ->
+  LexiconEngine.status * NCic.obj
+
+type pattern = 
+  CicNotationPt.term Disambiguate.disambiguator_input option * 
+  (string * NCic.term) list * NCic.term option
+
+val disambiguate_npattern:
+  GrafiteAst.npattern Disambiguate.disambiguator_input -> pattern
+    
+