Dead code for .moo files removed.

[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 4c7371e097da855f5d555403d51fbce89b5795db..ad88d5dfd11909e07d40ddeedea3462902537ea8 100644 (file)
--- a/matita/components/grafite_engine/grafiteEngine.mli
+++ b/matita/components/grafite_engine/grafiteEngine.mli
@@ -24,7 +24,6 @@
  *)
 
 exception Drop
-(*exception IncludedFileNotCompiled of string * string*)
 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
 
 type 'a disambiguator_input = string * int * 'a