notation on steroids: 'term 40 x' is a valid variable name in notation and

[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 f78507042e18d174c6a66f357d018cd99a2fe2f0..798fa75f528ed734f5e85db3ae9330156582ca29 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -43,9 +43,9 @@ val disambiguate_tactic:
 
 val disambiguate_command: 
  LexiconEngine.status ->
- baseuri:string option ->
+ ?baseuri:string ->
  Cic.metasenv ->
- ((CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
+ ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
   LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_macro: