.moo no longer used: all interesting data is left in either .lexicon or

[helm.git] / matita / components / grafite_engine / grafiteEngine.mli

diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli
index a6b9d7b1da247823c3726f0180c0ad74dd68b79a..4c7371e097da855f5d555403d51fbce89b5795db 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.mli
+++ b/matita/components/grafite_engine/grafiteEngine.mli
@@ -24,7 +24,7 @@
  *)
 
 exception Drop
-exception IncludedFileNotCompiled of string * string
+(*exception IncludedFileNotCompiled of string * string*)
 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 
 type 'a disambiguator_input = string * int * 'a