diff options
| author | emakarov | 2007-10-16 16:28:17 +0000 |
|---|---|---|
| committer | emakarov | 2007-10-16 16:28:17 +0000 |
| commit | d7e249dc1bfc2dd04ccf23c57b7ad40f1902568d (patch) | |
| tree | 543ff4b9aee9cb17b6d3f2239cbc1f6a3e931929 /configure | |
| parent | 201def788a3cac497134f460b90eb33bd5f80cce (diff) | |
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
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -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 |