- Procedural convertible rewrites in the conclusion are now detected and replaced...

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.mli

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index 1543387ee355af220bd16cef49974519505dfe82..f13fc418cd381ae6f20d36fe96fbb0f53887b1cf 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -54,3 +54,23 @@ val disambiguate_macro:
  Cic.context ->
  ((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
+    
+