Cic.term and Cic.obj unused!

[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 7590699f9412cab82aede8649e3378be45610417..e08908166e179f9fb6d8db6acf92c3604be4e9df 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.mli
+++ b/matita/components/grafite_parser/grafiteDisambiguate.mli
@@ -30,15 +30,11 @@ type tactic =
   NotationPt.term GrafiteAst.reduction, string) 
    GrafiteAst.tactic
 
-type lazy_tactic = 
-  (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) 
-    GrafiteAst.tactic
-
 val disambiguate_command: 
  LexiconEngine.status as 'status ->
  ?baseuri:string ->
- ((NotationPt.term,NotationPt.term NotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
-  'status * (Cic.term,Cic.obj) GrafiteAst.command
+ GrafiteAst.command Disambiguate.disambiguator_input ->
+  'status * GrafiteAst.command
 
 val disambiguate_nterm :
  NCic.term option ->