WARNING: partial commit.

[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 f12a973721475eb5d9a3c261e6001a3b6f8fc0f8..143ac5e11f83949682d513dfd51bb0f39328f4c1 100644 (file)
--- a/matita/components/grafite_parser/grafiteDisambiguate.ml
+++ b/matita/components/grafite_parser/grafiteDisambiguate.ml
@@ -25,7 +25,7 @@
 
 (* $Id$ *)
 
-class g_status =
+class type g_status =
   object
    inherit LexiconEngine.g_status
    inherit NCicCoercion.g_status