removed shift-reduce conflict

diff --git a/helm/software/components/binaries/tptp2grafite/Makefile b/helm/software/components/binaries/tptp2grafite/Makefile
index ad3557b7aab6730e8b0fd89044f368301f1a42e3..466861d51dc8aa2d1cd1a89342756b2a55858dbf 100644 (file)
--- a/helm/software/components/binaries/tptp2grafite/Makefile
+++ b/helm/software/components/binaries/tptp2grafite/Makefile
@@ -1,6 +1,6 @@
 all: tptp2grafite
 
-tptp2grafite:
+tptp2grafite: ast.ml parser.mly lexer.mll main.ml
        ocamlc -c ast.ml
        ocamlyacc parser.mly
        ocamlc -c parser.mli
@@ -11,4 +11,4 @@ tptp2grafite:
        ocamlc -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo
 
 clean:
-       rm -r tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml
+       rm -f tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml rm *.output

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