whelp and cic disambiguation removed

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

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.mli b/matita/components/grafite_parser/grafiteDisambiguate.mli
index 6565a4d9f0e4887091929e8fec214662597d6a1f..e17769ec98e2be2d0da4148490597dc26577581f 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -34,13 +34,6 @@ type lazy_tactic =
   (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
     GrafiteAst.tactic
 
-val disambiguate_tactic:
- LexiconEngine.status ref ->
- Cic.context ->
- Cic.metasenv -> int option ->
- tactic Disambiguate.disambiguator_input ->
-  Cic.metasenv * lazy_tactic
-
 val disambiguate_command: 
  LexiconEngine.status as 'status ->
  ?baseuri:string ->
@@ -48,13 +41,6 @@ val disambiguate_command:
  ((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 ->
- Cic.metasenv ->
- 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 -> 
  (#NEstatus.status as 'status) ->