X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftptp_grafite%2Fparser.mly;h=0f3525689212de5c2ae37b3a20d91363018f3afd;hb=95a14ced97592a4116485f94c6ffa806feb62dbc;hp=4fe172144a4a2636f11f0d840c42ed07fc9f0624;hpb=948bb5d710c5d7f3185b6fef76c8e71f247cc664;p=helm.git

diff --git a/helm/software/components/tptp_grafite/parser.mly b/helm/software/components/tptp_grafite/parser.mly
index 4fe172144..0f3525689 100644
--- a/helm/software/components/tptp_grafite/parser.mly
+++ b/helm/software/components/tptp_grafite/parser.mly
@@ -56,7 +56,12 @@
             name COMMA formula_type COMMA formula formula_source_and_infos 
           RPAREN DOT {
             AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
-      }
+	  }
+    | CNF LPAREN
+	  TYPE COMMA formula_type COMMA formula formula_source_and_infos
+	RPAREN DOT {
+	  AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
+	}
   ;
   
   formula_type: