Wrong invariant: Hypothesis (i.e. lambda-abstractions) can have no

[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 582ab11ec8afc0050e7058e256379e29e42ed58c..7a2e2dda877280596bbefae2bd39cbaa673eda98 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -45,8 +45,8 @@ val disambiguate_command:
  LexiconEngine.status ->
  baseuri:string option ->
  Cic.metasenv ->
- (CicNotationPt.obj GrafiteAst.command) Disambiguate.disambiguator_input ->
-  LexiconEngine.status * Cic.metasenv * Cic.obj GrafiteAst.command
+ ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
+  LexiconEngine.status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_macro:
  LexiconEngine.status ref ->