From d7e249dc1bfc2dd04ccf23c57b7ad40f1902568d Mon Sep 17 00:00:00 2001
From: emakarov
Date: Tue, 16 Oct 2007 16:28:17 +0000
Subject: Added transitivity and irreflexivity of <, as well as < -elimination
 for binary positive numbers.

Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 configure | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'configure')

diff --git a/configure b/configure
index 7962f27d8c..a8891856d1 100755
--- a/configure
+++ b/configure
@@ -399,24 +399,24 @@ esac
 # Very basic for the moment: if camlp5 exists, we use it...
 
 if [ "$camlp5dir" != "" ]; then
-    CAMLP4=camlp5
+    CAMLP4=$camlp5dir
     CAMLP4LIB=$camlp5dir
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
 elif [ "$CAMLTAG" = "OCAML310" ]; then
     if [ -x "${CAMLLIB}/camlp5" ]; then 
-        CAMLP4LIB=+camlp5
+	CAMLP4=camlp5
     elif [ -x "${CAMLLIB}/site-lib/camlp5" ]; then 
-        CAMLP4LIB=+site-lib/camlp5
+	CAMLP4=site-lib/camlp5
     else
 	echo "Objective Caml 3.10 found but no Camlp5 installed."
 	echo "Configuration script failed!"
 	exit 1
     fi
-    CAMLP4=camlp5
+    CAMLP4LIB=+$CAMLP4
     camlp4oexec=`echo $camlp4oexec | sed -e 's/4/5/'`
 else 
     CAMLP4=camlp4
-    CAMLP4LIB=+camlp4
+    CAMLP4LIB=+$CAMLP4
 fi
 
 if [ "$CAMLP4" = "camlp5" ] && `$camlp4oexec -v 2>&1 | grep -q 5.00`; then
-- 
cgit v1.2.3