aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/patches_coq/flocq.patch27
-rwxr-xr-xdev/build/windows/patches_coq/gappa_plugin.patch52
-rwxr-xr-xdev/build/windows/patches_coq/interval.patch38
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.
-