First attempt to implement unification hints.

[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 798fa75f528ed734f5e85db3ae9330156582ca29..1543387ee355af220bd16cef49974519505dfe82 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -37,7 +37,7 @@ 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
 
@@ -52,5 +52,5 @@ 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