make dependence on Menhir optional again

Makefile.in

@@ -62,6 +62,14 @@ else
   MENHIR = @MENHIR@
 endif
 
+ifeq (@enable_menhirlib@,yes)
+  MENHIRINC = -I +menhirLib
+  MENHIRLIB = menhirLib
+else
+  MENHIRINC =
+  MENHIRLIB =
+endif
+
 #PSVIEWER  = @PSVIEWER@
 #PDFVIEWER = @PDFVIEWER@
 
@@ -81,14 +89,7 @@ else
   DYNLINK =
 endif
 
-ifeq (@enable_menhirlib@,yes)
-  INCLUDES += -I +menhirLib
-  MENHIRLIB = menhirLib
-else
-  MENHIRLIB =
-endif
-
-EXTOBJS = $(MENHIRLIB)
+EXTOBJS =
 EXTLIBS = str unix nums $(DYNLINK)
 
 EXTCMA	= $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
@@ -146,7 +147,6 @@ LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
 ifeq (@enable_hypothesis_selection@,yes)
 	LIB_TRANSFORM += hypothesis_selection
 	INCLUDES += -I +ocamlgraph
-	LIBINCLUDES += -I +ocamlgraph
 	EXTLIBS += ocamlgraph/graph
 endif
 
@@ -156,7 +156,7 @@ LIBMLI = $(addsuffix .mli, $(LIBMODULES))
 LIBCMO = $(addsuffix .cmo, $(LIBMODULES))
 LIBCMX = $(addsuffix .cmx, $(LIBMODULES))
 
-$(LIBCMO) $(LIBCMX): INCLUDES = $(LIBINCLUDES)
+$(LIBCMO) $(LIBCMX): INCLUDES += $(LIBINCLUDES)
 $(LIBCMX): OFLAGS += -for-pack Why
 
 # build targets
@@ -242,7 +242,7 @@ PGMMLI = $(addsuffix .mli, $(PGMMODULES))
 PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
 PGMCMX = $(addsuffix .cmx, $(PGMMODULES))
 
-$(PGMCMO) $(PGMCMX): INCLUDES = -I src/programs
+$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
 
 # build targets
 
@@ -352,7 +352,7 @@ COQCMX = $(addsuffix .cmx, $(COQMODULES))
 COQTREES = kernel lib interp parsing proofs pretyping tactics library toplevel
 COQINCLUDES = -I src/coq-plugin $(addprefix -I @COQLIB@/, $(COQTREES))
 
-$(COQCMO) $(COQCMX): INCLUDES = $(COQINCLUDES)
+$(COQCMO) $(COQCMX): INCLUDES += $(COQINCLUDES)
 
 ifeq (@enable_coq_support@,yes)
 byte: src/coq-plugin/whytac.cma
@@ -410,8 +410,13 @@ $(TPTPCMO) $(TPTPCMX): INCLUDES += -I src/tptp2why
 
 # build targets
 
+ifeq (@enable_whytptp@,yes)
 byte: bin/whytptp.byte
 opt:  bin/whytptp.opt
+endif
+
+bin/whytptp.opt bin/whytptp.byte: EXTOBJS += $(MENHIRLIB)
+bin/whytptp.opt bin/whytptp.byte: INCLUDES += $(MENHIRINC)
 
 bin/whytptp.opt: src/why.cmxa $(TPTPCMX) src/main.cmx
 	$(if $(QUIET), @echo 'Linking  $@' &&) \
@@ -424,12 +429,14 @@ bin/whytptp.byte: src/why.cma $(TPTPCMO) src/main.cmo
 
 # depend and clean targets
 
+ifeq (@enable_whytptp@,yes)
 include .depend.tptp2why
 
 .depend.tptp2why: $(TPTPGENERATED)
 	$(OCAMLDEP) -slash -I src -I src/tptp2why $(TPTPML) $(TPTPMLI) > $@
 
 depend: .depend.tptp2why
+endif
 
 clean::
 	rm -f $(TPTPGENERATED)

configure.in

@@ -77,6 +77,12 @@ AC_ARG_ENABLE(coq-support,
     [  --enable-coq-support    enable Coq support],,
     enable_coq_support=yes)
 
+# TPTP parser
+
+AC_ARG_ENABLE(whytptp,
+    [  --enable-whytptp        enable TPTP parser (requires Menhir)],,
+    enable_whytptp=yes)
+
 # Menhir library
 
 AC_ARG_ENABLE(menhirlib,
@@ -213,11 +219,6 @@ if test "$OCAMLYACC" = no ; then
 	AC_MSG_ERROR(Cannot find ocamlyacc.)
 fi
 
-AC_CHECK_PROG(MENHIR,menhir,menhir,no)
-if test "$MENHIR" = no ; then
-	AC_MSG_ERROR(Cannot find menhir.)
-fi
-
 AC_CHECK_PROG(OCAMLDOC,ocamldoc,ocamldoc,true)
 if test "$OCAMLDOC" = true ; then
     AC_MSG_WARN(Cannot find ocamldoc)
@@ -230,6 +231,13 @@ fi
 
 AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)
 
+AC_CHECK_PROG(MENHIR,menhir,menhir,no)
+if test "$MENHIR" = no ; then
+    enable_whytptp=no
+    enable_menhirlib=no
+    AC_MSG_WARN(cannot find menhir.)
+fi
+
 # checking for libmenhir
 if test "$enable_menhirlib" = yes ; then
 AC_CHECK_FILE($OCAMLLIB/menhirLib,,enable_menhirlib=no)
@@ -329,6 +337,7 @@ AC_SUBST(COQDEP)
 AC_SUBST(COQLIB)
 AC_SUBST(COQVERSION)
 
+AC_SUBST(enable_whytptp)
 AC_SUBST(enable_menhirlib)
 
 AC_SUBST(enable_hypothesis_selection)
@@ -361,6 +370,7 @@ if test "$enable_coq_support" = "yes" ; then
    echo "    Version             : $COQVERSION"
    echo "    Lib                 : $COQLIB"
 fi
+echo "TPTP parser             : $enable_whytptp"
 echo "Menhir library          : $enable_menhirlib"
 echo "hypothesis selection    : $enable_hypothesis_selection"
 echo "profiling               : $ENABLE_PROFILING"