diff options
| author | Michael Soegtrop | 2019-07-19 12:01:59 +0200 |
|---|---|---|
| committer | Michael Soegtrop | 2019-07-19 12:01:59 +0200 |
| commit | 7341d286d4a9b440810097352fe257e476a8903c (patch) | |
| tree | 3237b7e25b45717102500295dd54b7f8e8b7905d /dev | |
| parent | b349791f7d683f25a79081082218d78fa01b408f (diff) | |
Removed patches for Flocq, Interval and Gappa (merged upstream)
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/build/windows/patches_coq/flocq.patch | 27 | ||||
| -rwxr-xr-x | dev/build/windows/patches_coq/gappa_plugin.patch | 52 | ||||
| -rwxr-xr-x | dev/build/windows/patches_coq/interval.patch | 38 |
3 files changed, 0 insertions, 117 deletions
diff --git a/dev/build/windows/patches_coq/flocq.patch b/dev/build/windows/patches_coq/flocq.patch deleted file mode 100755 index 33d909f47b..0000000000 --- a/dev/build/windows/patches_coq/flocq.patch +++ /dev/null @@ -1,27 +0,0 @@ -diff/patch file created on Sun, Jan 20, 2019 11:55:04 AM with: -difftar-folder.sh tarballs/Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.tar.gz Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e 1 -TARFILE= tarballs/Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.tar.gz -FOLDER= Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e -TARSTRIP= 1 -TARPREFIX= flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e/ -ORIGFOLDER= Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.orig ---- Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.orig/configure.in 2019-01-11 15:52:30.000000000 +0100 -+++ Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e/configure.in 2019-01-20 11:51:49.474668300 +0100 -@@ -10,7 +10,7 @@ - - m4_divert_push([HELP_ENABLE]) - Fine tuning of the installation directory: --AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Flocq@:>@]) -+AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Flocq@:>@]) - m4_divert_pop([HELP_ENABLE]) - - AC_PROG_CXX -@@ -51,7 +51,7 @@ - AC_MSG_RESULT([$COQDOC]) - - if test "$libdir" = '${exec_prefix}/lib'; then -- libdir="`$COQC -where`/user-contrib/Flocq" -+ libdir="`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Flocq" - fi - - AC_MSG_NOTICE([building remake...]) diff --git a/dev/build/windows/patches_coq/gappa_plugin.patch b/dev/build/windows/patches_coq/gappa_plugin.patch deleted file mode 100755 index 8bd32318d7..0000000000 --- a/dev/build/windows/patches_coq/gappa_plugin.patch +++ /dev/null @@ -1,52 +0,0 @@ -diff/patch file created on Sat, Jun 29, 2019 9:53:06 PM with: -difftar-folder.sh tarballs/gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.tar.gz gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e 1 -TARFILE= tarballs/gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.tar.gz -FOLDER= gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e -TARSTRIP= 1 -TARPREFIX= coq-04d859ea9a496f84569c3f9b8cb66784cd82313e/ -ORIGFOLDER= gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig ---- gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig/Remakefile.in 2019-04-09 16:57:15.000000000 +0200 -+++ gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e/Remakefile.in 2019-06-29 21:40:03.902985100 +0200 -@@ -43,7 +43,7 @@ - @COQC@ -R src Gappa -I src $< - - COQSUBTREES = clib engine kernel interp intf lib library ltac parsing pretyping printing proofs tactics toplevel vernac plugins/ltac --COQINCLUDES = $(addprefix -I @COQLIB@/, $(COQSUBTREES)) -+COQINCLUDES = $(addprefix -I "@COQLIB@"/, $(COQSUBTREES)) - - src/gappatac.cmo: src/gappatac.ml - @OCAMLC@ -pp "@CAMLP4O@ pa_macro.cmo -D@COQDEFINE@" -rectypes $(COQINCLUDES) -c $< -o $@ ---- gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig/configure.in 2019-04-09 16:57:15.000000000 +0200 -+++ gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e/configure.in 2019-06-29 21:47:31.294322200 +0200 -@@ -53,7 +53,17 @@ - if test ! "$CAMLP4O"; then - CAMLP4O=camlp5o - fi -- CAMLP4O=`which $CAMLP4O` -+ case `uname -s` in -+ CYGWIN*) -+ case "$CAMLP4O" in -+ *:*) CAMLP4O=`cygpath -m "$CAMLP4O"` ;; -+ *) CAMLP4O=`cygpath -u "$CAMLP4O"` ;; -+ esac -+ ;; -+ *) -+ CAMLP4O=`which $CAMLP4O` -+ ;; -+ esac - fi - AC_MSG_RESULT([$CAMLP4O]) - -@@ -81,10 +91,10 @@ - rm -f conftest.v conftest.vo conftest.err - - AC_SUBST(OCAMLLIB) --OCAMLLIB=`$OCAMLC -where` -+OCAMLLIB=`$OCAMLC -where | tr -d '\r' | tr '\\' '/'` - - AC_SUBST(COQLIB) --COQLIB=`$COQC -where` -+COQLIB=`$COQC -where | tr -d '\r' | tr '\\' '/'` - - if test "$libdir" = '${exec_prefix}/lib'; then - libdir="$COQLIB/user-contrib/Gappa" diff --git a/dev/build/windows/patches_coq/interval.patch b/dev/build/windows/patches_coq/interval.patch deleted file mode 100755 index 46b2b97826..0000000000 --- a/dev/build/windows/patches_coq/interval.patch +++ /dev/null @@ -1,38 +0,0 @@ -diff/patch file created on Sat, Jun 29, 2019 6:44:56 PM with: -difftar-folder.sh tarballs/interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.tar.gz interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628 1 -TARFILE= tarballs/interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.tar.gz -FOLDER= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628 -TARSTRIP= 1 -TARPREFIX= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/ -ORIGFOLDER= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig ---- interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig/configure.in 2019-04-09 17:31:18.000000000 +0200 -+++ interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/configure.in 2019-06-29 18:39:41.889749600 +0200 -@@ -10,7 +10,7 @@ - - m4_divert_push([HELP_ENABLE]) - Fine tuning of the installation directory: --AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Interval@:>@]) -+AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Interval@:>@]) - m4_divert_pop([HELP_ENABLE]) - - AC_PROG_CXX -@@ -79,7 +79,7 @@ - rm -f conftest.v conftest.vo conftest.err - - if test "$libdir" = '${exec_prefix}/lib'; then -- libdir="`$COQC -where`/user-contrib/Interval" -+ libdir="`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Interval" - fi - - AC_MSG_NOTICE([building remake...]) ---- interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig/src/Interval_missing.v 2019-04-09 17:31:18.000000000 +0200 -+++ interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/src/Interval_missing.v 2019-06-29 18:40:57.572496200 +0200 -@@ -1259,7 +1259,7 @@ - intros Heq Hb Hd. - apply (Rmult_eq_reg_r (b * d)). - field_simplify; trivial. --now rewrite Heq. -+try rewrite Heq. - now apply Rmult_neq0. - Qed. - |
