From 0e02c0fd09e2738a20e68855475bb309287ad485 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 12 May 2006 15:19:40 +0000
Subject: [PATCH] removed shift-reduce conflict

---
 .../components/binaries/tptp2grafite/Makefile       |  4 ++--
 .../components/binaries/tptp2grafite/parser.mly     | 13 ++++---------
 2 files changed, 6 insertions(+), 11 deletions(-)

diff --git a/helm/software/components/binaries/tptp2grafite/Makefile b/helm/software/components/binaries/tptp2grafite/Makefile
index ad3557b7a..466861d51 100644
--- 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 7d1c64336..05577000c 100644
--- 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 
-- 
2.39.2