X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fbinaries%2Ftptp2grafite%2Fparser.mly;h=05577000cf650f214a101af4f2a8a1d23b1e0d1e;hb=81b53ddc3ce92187e62deff483919ca2251fd246;hp=7d1c6433635a44c402766d4a4e2da71b5f90db2e;hpb=3bb48c9cb4c33a8fc457e6835fbf157f12545047;p=helm.git

diff --git a/components/binaries/tptp2grafite/parser.mly b/components/binaries/tptp2grafite/parser.mly
index 7d1c64336..05577000c 100644
--- a/components/binaries/tptp2grafite/parser.mly
+++ b/components/binaries/tptp2grafite/parser.mly
@@ -53,9 +53,9 @@
  
   annot_formula: 
     | CNF LPAREN 
-            name COMMA formula_type COMMA formula formula_source formula_infos 
+            name COMMA formula_type COMMA formula formula_source_and_infos 
           RPAREN DOT {
-            AnnotatedFormula ($3,$5,$7,$8,$9)  
+            AnnotatedFormula ($3,$5,$7,fst $8,snd $8)  
       }
   ;
   
@@ -121,16 +121,11 @@
     | QSTRING { rm_q $1 }
   ;
   
-  formula_source:
-    | { NoSource }
+  formula_source_and_infos:
+        | { NoSource, [NoInfo] }
     | COMMA { assert false }
   ;
     
-  formula_infos:
-    | { [NoInfo] }
-    | COMMA { assert false }
-  ;
-  
   include_: 
     | INCLUSION LPAREN QSTRING selection_of_formulae RPAREN DOT {
         let fname = rm_q $3 in