bugfix to developments:

[helm.git] / components / binaries / tptp2grafite / parser.mly

diff --git a/components/binaries/tptp2grafite/parser.mly b/components/binaries/tptp2grafite/parser.mly
index 7d1c6433635a44c402766d4a4e2da71b5f90db2e..05577000cf650f214a101af4f2a8a1d23b1e0d1e 100644 (file)
--- 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