- cic almost not used

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

diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml
index c23e5acffd9d7270cd344fb18064e87409d1c550..bd633d5d2edb26057068c8ee0f8c3dc7146971a3 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -32,10 +32,6 @@ 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
-
 let singleton msg = function
   | [x], _ -> x
   | l, _   ->