Stricter type: the type now shows that disambiguation only alter the lexicon.

[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 0592de671e9fe18cd2c75398248ce12588c5cae5..6565a4d9f0e4887091929e8fec214662597d6a1f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -35,21 +35,21 @@ type lazy_tactic =
     GrafiteAst.tactic
 
 val disambiguate_tactic:
- #LexiconEngine.status ref ->
+ LexiconEngine.status ref ->
  Cic.context ->
  Cic.metasenv -> int option ->
  tactic Disambiguate.disambiguator_input ->
   Cic.metasenv * lazy_tactic
 
 val disambiguate_command: 
- #NEstatus.status as 'status ->
+ LexiconEngine.status as 'status ->
  ?baseuri:string ->
  Cic.metasenv ->
  ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
   'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_macro:
- #LexiconEngine.status ref ->
+ LexiconEngine.status ref ->
  Cic.metasenv ->
  Cic.context ->
  ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->