Merge branch 'v8.6'

36 files changed, 3335 insertions, 420 deletions

diff --git a/dev/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index b43ada907..b43ada907 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
diff --git a/dev/build/windows/CAVEATS.txt b/dev/build/windows/CAVEATS.txt
new file mode 100644
index 000000000..cb1ae3aaa
--- /dev/null
+++ b/dev/build/windows/CAVEATS.txt
@@ -0,0 +1,22 @@
+===== Environemt SIZE =====

+

+find and xargs can fail if the environment is to large. I think the limit is 8k.

+

+xargs --show-limits

+

+shows the actual environment size

+

+The configure_profile.sh script sets ORIGINAL_PATH (set by cygwin) to "" to

+avoid issues

+

+===== OCAMLLIB =====

+

+If the environment variable OCAMLLIB is defined, it takes precedence over the

+internal paths of ocaml tools. This usually messes up things considerably. A

+typical failure is

+

+Error: Error on dynamically loaded library: .\dlllablgtk2.dll: %1 is not a valid Win32 application.

+

+The configure_profile.sh script clears OCAMLLIB, but if you use the ocaml

+compiler from outside the provided cygwin shell, OCAMLLIB might be defined.

+

diff --git a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
new file mode 100644
index 000000000..bdcb01db9
--- /dev/null
+++ b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
@@ -0,0 +1,10 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -mode=absolute ^

+  -ocaml=Y ^

+  -make=Y ^

+  -coqver=8.4pl6 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_84pl6_abs ^

+  -destcoq=%ROOTPATH%\coq64_84pl6_abs

diff --git a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
new file mode 100644
index 000000000..2e4a692e9
--- /dev/null
+++ b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
@@ -0,0 +1,10 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -mode=absolute ^

+  -ocaml=Y ^

+  -make=Y ^

+  -coqver=8.5pl2 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_85pl2_abs ^

+  -destcoq=%ROOTPATH%\coq64_85pl2_abs

diff --git a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
new file mode 100644
index 000000000..6e4e440a2
--- /dev/null
+++ b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
@@ -0,0 +1,10 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -mode=absolute ^

+  -ocaml=Y ^

+  -make=Y ^

+  -coqver=8.5pl3 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_85pl3_abs ^

+  -destcoq=%ROOTPATH%\coq64_85pl3_abs

diff --git a/dev/build/windows/MakeCoq_85pl3_installer.bat b/dev/build/windows/MakeCoq_85pl3_installer.bat
new file mode 100644
index 000000000..c305e2f52
--- /dev/null
+++ b/dev/build/windows/MakeCoq_85pl3_installer.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -installer=Y ^

+  -coqver=8.5pl3 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_85pl3_inst ^

+  -destcoq=%ROOTPATH%\coq64_85pl3_inst

diff --git a/dev/build/windows/MakeCoq_85pl3_installer_32.bat b/dev/build/windows/MakeCoq_85pl3_installer_32.bat
new file mode 100644
index 000000000..d87ff5919
--- /dev/null
+++ b/dev/build/windows/MakeCoq_85pl3_installer_32.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=32 ^

+  -installer=Y ^

+  -coqver=8.5pl3 ^

+  -destcyg=%ROOTPATH%\cygwin_coq32_85pl3_inst ^

+  -destcoq=%ROOTPATH%\coq32_85pl3_inst

diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
new file mode 100644
index 000000000..f1d855a02
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
@@ -0,0 +1,10 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -mode=absolute ^

+  -ocaml=Y ^

+  -make=Y ^

+  -coqver=git-v8.6 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_86git_abs ^

+  -destcoq=%ROOTPATH%\coq64_86git_abs

diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
new file mode 100644
index 000000000..70ab42bc3
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
@@ -0,0 +1,11 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -mode=absolute ^

+  -ocaml=Y ^

+  -make=Y ^

+  -gtksrc=Y ^

+  -coqver=git-v8.6 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_86git_abs_gtksrc ^

+  -destcoq=%ROOTPATH%\coq64_86git_abs_gtksrc

diff --git a/dev/build/windows/MakeCoq_86git_installer.bat b/dev/build/windows/MakeCoq_86git_installer.bat
new file mode 100644
index 000000000..40506318e
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_installer.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -installer=Y ^

+  -coqver=git-v8.6 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_86git_inst ^

+  -destcoq=%ROOTPATH%\coq64_86git_inst

diff --git a/dev/build/windows/MakeCoq_86git_installer2.bat b/dev/build/windows/MakeCoq_86git_installer2.bat
new file mode 100644
index 000000000..d184f0e30
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_installer2.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -installer=Y ^

+  -coqver=git-v8.6 ^

+  -destcyg=%ROOTPATH%\cygwin_coq64_86git_inst2 ^

+  -destcoq=%ROOTPATH%\coq64_86git_inst2

diff --git a/dev/build/windows/MakeCoq_86git_installer_32.bat b/dev/build/windows/MakeCoq_86git_installer_32.bat
new file mode 100644
index 000000000..b9127c945
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_installer_32.bat
@@ -0,0 +1,8 @@
+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=32 ^

+  -installer=Y ^

+  -coqver=git-v8.6 ^

+  -destcyg=%ROOTPATH%\cygwin_coq32_86git_inst ^

+  -destcoq=%ROOTPATH%\coq32_86git_inst

diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
new file mode 100644
index 000000000..1e08cc5a3
--- /dev/null
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -0,0 +1,445 @@
+@ECHO OFF
+
+REM ========== COPYRIGHT/COPYLEFT ==========
+
+REM (C) 2016 Intel Deutschland GmbH
+REM Author: Michael Soegtrop
+
+REM Released to the public by Intel under the
+REM GNU Lesser General Public License Version 2.1 or later
+REM See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+
+REM ========== NOTES ==========
+
+REM For Cygwin setup command line options
+REM see https://cygwin.com/faq/faq.html#faq.setup.cli
+
+REM ========== DEFAULT VALUES FOR PARAMETERS ==========
+
+REM For a description of all parameters, see ReadMe.txt
+
+SET BATCHFILE=%0
+SET BATCHDIR=%~dp0
+
+REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
+SET ARCH=x86_64
+
+REM see -mode in ReadMe.txt
+SET INSTALLMODE=absolute
+
+REM see -installer in ReadMe.txt
+SET MAKEINSTALLER=N
+
+REM see -ocaml in ReadMe.txt
+SET INSTALLOCAML=N
+
+REM see -make in ReadMe.txt
+SET INSTALLMAKE=Y
+
+REM see -destcyg in ReadMe.txt
+SET DESTCYG=C:\bin\cygwin_coq
+
+REM see -destcoq in ReadMe.txt
+SET DESTCOQ=C:\bin\coq
+
+REM see -setup in ReadMe.txt
+SET SETUP=setup-x86_64.exe
+
+REM see -proxy in ReadMe.txt
+IF DEFINED HTTP_PROXY (
+  SET PROXY="%HTTP_PROXY:http://=%"
+) else (
+  SET PROXY=""
+)
+
+REM see -cygrepo in ReadMe.txt
+SET CYGWIN_REPOSITORY=http://ftp.inf.tu-dresden.de/software/windows/cygwin32
+
+REM see -cygcache in ReadMe.txt
+SET CYGWIN_LOCAL_CACHE_WFMT=%BATCHDIR%cygwin_cache
+
+REM see -cyglocal in ReadMe.txt
+SET CYGWIN_FROM_CACHE=N
+
+REM see -cygquiet in ReadMe.txt
+SET CYGWIN_QUIET=Y
+
+REM see -srccache in ReadMe.txt
+SET SOURCE_LOCAL_CACHE_WFMT=%BATCHDIR%source_cache
+
+REM see -coqver in ReadMe.txt
+SET COQ_VERSION=8.5pl3
+
+REM see -gtksrc in ReadMe.txt
+SET GTK_FROM_SOURCES=N
+
+REM see -threads in ReadMe.txt
+SET MAKE_THREADS=8
+
+REM ========== PARSE COMMAND LINE PARAMETERS ==========
+
+SHIFT
+
+:Parse
+
+IF "%0" == "-arch" (
+  IF "%1" == "32" (
+    SET ARCH=i686
+    SET SETUP=setup-x86.exe
+  ) ELSE (
+    IF "%1" == "64" (
+      SET ARCH=x86_64
+      SET SETUP=setup-x86_64.exe
+    ) ELSE (
+      ECHO "Invalid -arch, valid are 32 and 64"
+      GOTO :EOF
+    )
+  )
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-mode" (
+  IF "%1" == "mingwincygwin" (
+    SET INSTALLMODE=%1
+  ) ELSE (
+    IF "%1" == "absolute" (
+      SET INSTALLMODE=%1
+    ) ELSE (
+      IF "%1" == "relocatable" (
+        SET INSTALLMODE=%1
+      ) ELSE (
+        ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
+        GOTO :EOF
+      )
+    )
+  )
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-installer" (
+  SET MAKEINSTALLER=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-ocaml" (
+  SET INSTALLOCAML=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-make" (
+  SET INSTALLMAKE=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-destcyg" (
+  SET DESTCYG=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-destcoq" (
+  SET DESTCOQ=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-setup" (
+  SET SETUP=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-proxy" (
+  SET PROXY="%1"
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-cygrepo" (
+  SET CYGWIN_REPOSITORY="%1"
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-cygcache" (
+  SET CYGWIN_LOCAL_CACHE_WFMT="%1"
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-cyglocal" (
+  SET CYGWIN_FROM_CACHE=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-cygquiet" (
+  SET CYGWIN_QUIET=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-srccache" (
+  SET SOURCE_LOCAL_CACHE_WFMT="%1"
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-coqver" (
+  SET COQ_VERSION=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-gtksrc" (
+  SET GTK_FROM_SOURCES=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF "%0" == "-threads" (
+  SET MAKE_THREADS=%1
+  SHIFT
+  SHIFT
+  GOTO Parse
+)
+
+IF NOT "%0" == "" (
+  ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
+  ECHO !!! Illegal parameter %0
+  ECHO Usage: 
+  ECHO MakeCoq_MinGW
+  CALL :PrintPars
+  goto :EOF
+)
+
+IF NOT EXIST %SETUP% (
+  ECHO The cygwin setup program %SETUP% doesn't exist. You must download it from https://cygwin.com/install.html.
+  GOTO :EOF
+)
+
+REM ========== ADJUST PARAMETERS ==========
+
+IF "%INSTALLMODE%" == "mingwincygwin" (
+  SET DESTCOQ=%DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw
+)
+
+IF "%MAKEINSTALLER%" == "Y" (
+  SET INSTALLMODE=relocatable
+  SET INSTALLOCAML=Y
+  SET INSTALLMAKE=Y
+)
+
+REM ========== CONFIRM PARAMETERS ==========
+
+CALL :PrintPars
+REM Note: DOS batch replaces variables on parsing, so one can't use a variable just set in an () block
+IF "%COQREGTESTING%"=="Y" (GOTO :DontAsk)
+  SET /p ANSWER=Is this correct? y/n 
+  IF NOT "%ANSWER%"=="y" (GOTO :EOF)
+:DontAsk
+
+REM ========== DERIVED VARIABLES ==========
+
+SET CYGWIN_INSTALLDIR_WFMT=%DESTCYG%
+SET RESULT_INSTALLDIR_WFMT=%DESTCOQ%
+SET TARGET_ARCH=%ARCH%-w64-mingw32
+SET BASH=%CYGWIN_INSTALLDIR_WFMT%\bin\bash
+
+REM Convert pathes to various formats
+REM WFMT = windows format (C:\..)          Used in this batch file.
+REM CFMT = cygwin format (\cygdrive\c\..)  Used for Cygwin PATH varible, which is : separated, so C: doesn't work.
+REM MFMT = MinGW format (C:/...)           Used for the build, because \\ requires escaping. Mingw can handle \ and /.
+
+SET CYGWIN_INSTALLDIR_MFMT=%CYGWIN_INSTALLDIR_WFMT:\=/%
+SET RESULT_INSTALLDIR_MFMT=%RESULT_INSTALLDIR_WFMT:\=/%
+SET SOURCE_LOCAL_CACHE_MFMT=%SOURCE_LOCAL_CACHE_WFMT:\=/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_MFMT:C:/=/cygdrive/c/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_MFMT:C:/=/cygdrive/c/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:D:/=/cygdrive/d/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:D:/=/cygdrive/d/%
+
+SET CYGWIN_INSTALLDIR_CFMT=%CYGWIN_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET RESULT_INSTALLDIR_CFMT=%RESULT_INSTALLDIR_CFMT:E:/=/cygdrive/e/%
+SET SOURCE_LOCAL_CACHE_CFMT=%SOURCE_LOCAL_CACHE_CFMT:E:/=/cygdrive/e/%
+
+ECHO CYGWIN INSTALL DIR (WIN)    = %CYGWIN_INSTALLDIR_WFMT%
+ECHO CYGWIN INSTALL DIR (MINGW)  = %CYGWIN_INSTALLDIR_MFMT%
+ECHO CYGWIN INSTALL DIR (CYGWIN) = %CYGWIN_INSTALLDIR_CFMT%
+ECHO RESULT INSTALL DIR (WIN)    = %RESULT_INSTALLDIR_WFMT%
+ECHO RESULT INSTALL DIR (MINGW)  = %RESULT_INSTALLDIR_MFMT%
+ECHO RESULT INSTALL DIR (CYGWIN) = %RESULT_INSTALLDIR_CFMT%
+
+REM WARNING: Add a space after the = in case you want set this to empty, otherwise the variable will be unset
+SET MAKE_OPT=-j %MAKE_THREADS% 
+
+REM ========== DERIVED CYGWIN SETUP OPTIONS ==========
+
+REM WARNING: Add a space after the = otherwise the variable will be unset
+SET CYGWIN_OPT= 
+
+IF "%CYGWIN_FROM_CACHE%" == "Y" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -L
+)
+
+IF "%CYGWIN_QUIET%" == "Y" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -q --no-admin
+)
+
+IF "%GTK_FROM_SOURCES%"=="N" (
+  SET CYGWIN_OPT= %CYGWIN_OPT% -P mingw64-%ARCH%-gtk2.0,mingw64-%ARCH%-gtksourceview2.0
+)
+
+ECHO ========== INSTALL CYGWIN ==========
+
+REM Cygwin setup sets proper ACLs (permissions) for folders it CREATES.
+REM Otherwise chmod won't work and e.g. the ocaml build will fail.
+REM Cygwin setup does not touch the ACLs of existing folders.
+REM => Create the setup log in a temporary location and move it later.
+
+REM Get Unique temporary file name
+:logfileloop
+SET LOGFILE=%TEMP%\CygwinSetUp%RANDOM%-%RANDOM%-%RANDOM%-%RANDOM%.log
+if exist "%LOGFILE%" goto :logfileloop
+
+REM Run Cygwin Setup
+
+SET RUNSETUP=Y
+IF EXIST "%CYGWIN_INSTALLDIR_WFMT%\etc\setup\installed.db" (
+  SET RUNSETUP=N
+)
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+  SET RUNSETUP=Y
+)
+
+IF "%RUNSETUP%"=="Y" (
+  %SETUP% ^
+    --proxy %PROXY% ^
+    --site %CYGWIN_REPOSITORY% ^
+    --root %CYGWIN_INSTALLDIR_WFMT% ^
+    --local-package-dir %CYGWIN_LOCAL_CACHE_WFMT% ^
+    --no-shortcuts ^
+    %CYGWIN_OPT% ^
+    -P wget,curl,git,make,unzip ^
+    -P gcc-core,gcc-g++ ^
+    -P gdb,liblzma5 ^
+    -P patch,automake1.14,automake1.15 ^
+    -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-pkg-config,mingw64-%ARCH%-windows_default_manifest ^
+    -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+    -P libiconv-devel,libunistring-devel,libncurses-devel ^
+    -P gettext-devel,libgettextpo-devel ^
+    -P libglib2.0-devel,libgdk_pixbuf2.0-devel ^
+    -P libfontconfig1 ^
+    -P gtk-update-icon-cache ^
+    -P libtool,automake ^
+    -P intltool ^
+    > "%LOGFILE%" ^
+    || GOTO :Error
+
+  MKDIR %CYGWIN_INSTALLDIR_WFMT%\build
+  MKDIR %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs
+  MOVE  "%LOGFILE%" %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log || GOTO :Error
+)
+
+
+IF NOT "%CYGWIN_QUIET%" == "Y" (
+  REM Like most setup programs, cygwin setup starts the real setup as a separate process, so wait for it.
+  REM This is not required with the -cygquiet=Y and the resulting --no-admin option.
+  :waitsetup
+  tasklist /fi "imagename eq %SETUP%" | find ":" > NUL
+  IF ERRORLEVEL 1 GOTO waitsetup
+)
+
+ECHO ========== CONFIGURE CYGWIN USER ACCOUNT ==========
+
+copy %BATCHDIR%\configure_profile.sh %CYGWIN_INSTALLDIR_WFMT%\var\tmp || GOTO :Error
+%BASH% --login %CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh %PROXY% || GOTO :Error
+
+ECHO ========== BUILD COQ ==========
+
+MKDIR %CYGWIN_INSTALLDIR_WFMT%\build
+MKDIR %CYGWIN_INSTALLDIR_WFMT%\build\patches
+
+COPY %BATCHDIR%\makecoq_mingw.sh    %CYGWIN_INSTALLDIR_WFMT%\build || GOTO :Error
+COPY %BATCHDIR%\patches_coq\*.* %CYGWIN_INSTALLDIR_WFMT%\build\patches || GOTO :Error
+
+%BASH% --login %CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh || GOTO :Error
+
+ECHO ========== FINISHED ==========
+
+GOTO :EOF
+
+ECHO ========== BATCH FUNCTIONS ==========
+
+:PrintPars
+  REM  01234567890123456789012345678901234567890123456789012345678901234567890123456789
+  ECHO -arch     ^<i686 or x86_64^> Set cygwin, ocaml and coq to 32 or 64 bit
+  ECHO -mode     ^<mingwincygwin = install coq in default cygwin mingw sysroot^>
+  ECHO           ^<absoloute = install coq in -destcoq absulute path^>
+  ECHO           ^<relocatable = install relocatable coq in -destcoq path^>
+  ECHO -installer^<Y or N^> create a windows installer (will be in /build/coq/dev/nsis)
+  ECHO -ocaml    ^<Y or N^> install OCaml in Coq folder (Y) or just in cygwin folder (N)
+  ECHO -make     ^<Y or N^> install GNU Make in Coq folder (Y) or not (N)
+  ECHO -destcyg  ^<path to cygwin destination folder^>
+  ECHO -destcoq  ^<path to coq destination folder (mode=absoloute/relocatable)^>
+  ECHO -setup    ^<cygwin setup program name^> (auto adjusted to -arch)
+  ECHO -proxy    ^<internet proxy^>
+  ECHO -cygrepo  ^<cygwin download repository^>
+  ECHO -cygcache ^<local cygwin repository/cache^>
+  ECHO -cyglocal ^<Y or N^> install cygwin from cache 
+  ECHO -cygquiet ^<Y or N^> install cygwin without user interaction
+  ECHO -srccache ^<local source code repository/cache^>
+  ECHO -coqver   ^<Coq version to install^> 
+  ECHO -gtksrc   ^<Y or N^> build GTK ^(90 min^) or use cygwin version
+  ECHO -threads  ^<1..N^> Number of make threads
+  ECHO(
+  ECHO See ReadMe.txt for a detailed description of all parameters
+  ECHO(
+  ECHO Parameter values (default or currently set):
+  ECHO -arch     = %ARCH%
+  ECHO -mode     = %INSTALLMODE%
+  ECHO -ocaml    = %INSTALLOCAML%
+  ECHO -installer= %MAKEINSTALLER%
+  ECHO -make     = %INSTALLMAKE%
+  ECHO -destcyg  = %DESTCYG% 
+  ECHO -destcoq  = %DESTCOQ% 
+  ECHO -setup    = %SETUP% 
+  ECHO -proxy    = %PROXY%
+  ECHO -cygrepo  = %CYGWIN_REPOSITORY%
+  ECHO -cygcache = %CYGWIN_LOCAL_CACHE_WFMT%
+  ECHO -cyglocal = %CYGWIN_FROM_CACHE%
+  ECHO -cygquiet = %CYGWIN_QUIET%
+  ECHO -srccache = %SOURCE_LOCAL_CACHE_WFMT%
+  ECHO -coqver   = %COQ_VERSION%
+  ECHO -gtksrc   = %GTK_FROM_SOURCES%
+  ECHO -threads  = %MAKE_THREADS%
+  GOTO :EOF
+
+:Error
+ECHO Building Coq failed with error code %errorlevel%
+EXIT /b %errorlevel%
diff --git a/dev/build/windows/MakeCoq_SetRootPath.bat b/dev/build/windows/MakeCoq_SetRootPath.bat
new file mode 100644
index 000000000..3a3711724
--- /dev/null
+++ b/dev/build/windows/MakeCoq_SetRootPath.bat
@@ -0,0 +1,16 @@
+@ ECHO OFF
+
+REM Figure out a root path for coq and cygwin
+
+REM For the \nul trick for testing folders see
+REM https://support.microsoft.com/en-us/kb/65994
+
+IF EXIST D:\bin\nul (
+  SET ROOTPATH=D:\bin
+) else if EXIST C:\bin (
+  SET ROOTPATH=C:\bin
+) else (
+  SET ROOTPATH=C:
+)
+
+ECHO ROOTPATH set to %ROOTPATH%
diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat
new file mode 100644
index 000000000..2b0b83fed
--- /dev/null
+++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat
@@ -0,0 +1,18 @@
+call MakeCoq_SetRootPath

+

+SET HTTP_PROXY=

+EXPORT HTTP_PROXY=

+MKDIR C:\Temp\srccache

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -mode=absolute ^

+  -ocaml=Y ^

+  -make=Y ^

+  -coqver 8.5pl2 ^

+  -srccache C:\Temp\srccache ^

+  -cygquiet=Y ^

+  -destcyg   %ROOTPATH%\cygwin_coq64_85pl2_abs ^

+  -destcoq   %ROOTPATH%\coq64_85pl2_abs

+
+pause
\ No newline at end of file
diff --git a/dev/build/windows/MakeCoq_regtests.bat b/dev/build/windows/MakeCoq_regtests.bat
new file mode 100644
index 000000000..6e36d0140
--- /dev/null
+++ b/dev/build/windows/MakeCoq_regtests.bat
@@ -0,0 +1,16 @@
+SET COQREGTESTING=Y
+
+REM Bleeding edge
+call MakeCoq_86git_abs_ocaml.bat
+call MakeCoq_86git_installer.bat
+call MakeCoq_86git_installer_32.bat
+call MakeCoq_86git_abs_ocaml_gtksrc.bat
+
+REM Current stable
+call MakeCoq_85pl3_abs_ocaml.bat
+call MakeCoq_85pl3_installer.bat
+call MakeCoq_85pl3_installer_32.bat
+
+REM Old but might still be used
+call MakeCoq_85pl2_abs_ocaml.bat
+call MakeCoq_84pl6_abs_ocaml.bat
diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
new file mode 100644
index 000000000..0faf5bc53
--- /dev/null
+++ b/dev/build/windows/ReadMe.txt
@@ -0,0 +1,460 @@
+==================== Purpose / Goal ====================
+
+The main purpose of these scripts is to build Coq for Windows in a reproducible
+and at least by this script documented way without using binary libraries and
+executables from various sources. These scripts use only MinGW libraries
+provided by Cygwin or compile things from sources. For some libraries there are
+options to build them from sources or to use the Cygwin version.
+
+Another goal (which is not yet achieved) is to have a Coq installer for
+Windows, which includes all tools required for native compute and Coq plugin
+development without Cygwin.
+
+Coq requires OCaml for this and OCaml requires binutils, gcc and a posix shell.
+Since the standard Windows OCaml installation requires Cygwin to deliver some of
+these components, you might be able to imagine that this is not so easy.
+
+These scripts can produce the following:
+
+- Coq running on MinGW
+
+- OCaml producing MinGW code and running on MinGW
+
+- GCC producing MinGW code and running on MinGW
+
+- binutils producing MinGW code and running on MinGW
+
+With "running on MinGW" I mean that the tools accept paths like
+"C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys DLL. The
+MinGW gcc and binutils provided by Cygwin produce MinGW code, but they run only
+on Cygwin.
+
+With "producing MinGW code" I mean that the programs created by the tools accept
+paths like "C:\myfolder\myfile.txt" and that they don't link to a Cygwin or msys
+DLL.
+
+The missing piece is a posix shell running on plain Windows (without msys or
+Cygwin DLL) and not beeing a binary from obscure sources. I am working on it ...
+
+Since compiling gcc and binutils takes a while and it is not of much use without
+a shell, the building of these components is currently disabled. OCaml is built
+anyway, because this MinGW/MinGW OCaml (rather than a Cygwin/MinGW OCaml) is
+used to compile Coq.
+
+Until the shell is there, the Cygwin created by these scripts is required to run
+OCaml tools. When everything is finished, this will no longer be required.
+
+==================== Usage ====================
+
+The Script MakeCoq_MinGW does:
+- download Cygwin (except the Setup.exe or Setup64.exe)
+- install Cygwin
+- either installs MinGW GTK via Cygwin or compiles it fom sources
+- download, compile and install OCaml, CamlP5, Menhir, lablgtk
+- download, compile and install Coq
+- create a Windows installer (NSIS based)
+
+The parameters are described below. Mostly paths and the HTTP proxy need to be
+set.
+
+There are two main usages:
+
+- Compile and install OCaml and Coq in a given folder
+
+  This works reliably, because absolute library paths can be compiled into Coq
+  and OCaml.
+  
+  WARNING: See the "Purpose / Goal" section above for status.
+  
+  See MakeCoq_85pl2_abs_ocaml.bat for parameters.
+
+- Create a Windows installer.
+
+  This works well for Coq but not so well for OCaml.
+
+  WARNING: See the "Purpose / Goal" section above for status.
+  
+  See MakeCoq_85pl2_installer.bat for parameters.
+
+There is also an option to compile OCaml and Coq inside Cygwin, but this is
+currently not recommended. The resulting Coq and OCaml work, but Coq is slow
+because it scans the largish Cygwin share folder. This will be fixed in a future
+version.
+
+Procedure:
+
+- Unzip contents of CoqSetup.zip in a folder
+
+- Adjust parameters in MakeCoq_85pl2_abs_ocaml.bat or in MakeCoq_85pl2_installer.bat.
+
+- Download Cygwin setup from https://Cygwin.com/install.html
+  For 32 bit Coq : setup-x86.exe    (https://Cygwin.com/setup-x86.exe)
+  For 64 bit Coq : setup-x86_64.exe (https://Cygwin.com/setup-x86_64.exe)
+
+- Run MakeCoq_85pl3_abs_ocaml.bat or MakeCoq_85pl3_installer.bat
+
+- Check MakeCoq_regtests.bat to see what combinations of options are tested
+
+==================== MakeCoq_MinGW Parameters ====================
+
+===== -arch =====
+
+Set the target architecture.
+
+Possible values:
+
+32: Install/build Cygwin, ocaml and coq for 32 bit windows
+
+64: Install/build Cygwin, ocaml and coq for 64 bit windows
+
+Default value: 64
+
+
+===== -mode =====
+
+Set the installation mode / target folder structure.
+  
+Possible values:
+
+mingwinCygwin: Install coq in the default Cygwin mingw sysroot folder.
+               This is %DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw.
+               Todo: The coq share folder should be configured to e.g. /share/coq.
+               As is, coqc scans the complete share folder, which slows it down 5x for short files.
+               
+absoloute:     Install coq in the absolute path given with -destcoq.
+               The resulting Coq will not be relocatable.
+               That is the root folder must not be renamed/moved.
+
+relocatable:   Install coq in the absolute path given with -destcoq.
+               The resulting Coq will be relocatable.
+               That is the root folder may be renamed/moved.
+               If OCaml is installed, please note that OCaml cannot be build really relocatable.
+               If the root folder is moved, the environment variable OCAMLLIB must be set to the libocaml sub folder.
+               Also the file <root>\libocaml\ld.conf must be adjusted.
+
+Default value: absolute
+
+
+===== -installer =====
+
+Create a Windows installer (it will be in build/coq-8.xplx/dev/nsis)
+
+Possible values:
+
+Y: Create a windows installer - this forces -mode=relocatable.
+
+N: Don't create a windows installer - use the created Coq installation as is.
+
+Default value: N
+
+
+===== -ocaml =====
+
+Install OCaml for later use with Coq or just for building.
+
+Possible values:
+
+Y: Install OCaml in the same root as Coq (as given with -coqdest)
+   This also copies all .o, .cmo, .a, .cmxa files in the lib folder required for compiling plugins.
+
+N: Install OCaml in the default Cygwin mingw sysroot folder.
+   This is %DESTCYG%\usr\%ARCH%-w64-mingw32\sys-root\mingw.
+
+Default value: N
+
+
+===== -make =====
+
+Build and install MinGW GNU make
+
+Possible values:
+
+Y: Install MinGW GNU make in the same root as Coq (as given with -coqdest).
+
+N: Don't build or install MinGW GNU make.
+   For building everything always Cygwin GNU make is used.
+
+Default value: Y
+
+
+===== -destcyg =====
+
+Destination folder in which Cygwin is installed.
+
+This must be an absolute path in Windows format (with drive letter and \\).
+
+>>>>> This folder may be deleted after the Coq build is finished! <<<<<
+
+Default value: C:\bin\Cygwin_coq
+
+
+===== -destcoq =====
+
+Destination folder in which Coq is installed.
+
+This must be an absolute path in Windows format (with drive letter and \\).
+
+This option is not required if -mode mingwinCygwin is used.
+
+Default value: C:\bin\coq
+
+
+===== -setup =====
+
+Name/path of the Cygwin setup program.
+
+The Cygwin setup program is called setup-x86.exe or setup-x86_64.exe.
+It can be downloaded from: https://Cygwin.com/install.html.
+
+Default value: setup-x86.exe or setup-x86_64.exe, depending on -arch.
+
+
+===== -proxy =====
+
+Internet proxy setting for downloading Cygwin, ocaml and coq.
+
+The format is <server>:<port>, e.g. proxy.mycompany.com:911
+
+The same proxy is used for HTTP, HTTPS and FTP.
+If you need separate proxies for separate protocols, you please put your proxies directly into configure_profile.sh (line 11..13).
+
+Default value: Value of HTTP_PROXY environment variable or none if this variable does not exist.
+
+ATTENTION: With the --proxy setting of the Cygwin setup, it is possible to
+supply a proxy server, but if this parameter is "", Cygwin setup might use proxy
+settings from previous setups. If you once did a Cygwin setup behind a firewall
+and now want to do a Cygwin setup without a firewall, use the -cygquiet=N
+setting to perform a GUI install, where you can adjust the proxy setting.
+
+===== -cygrepo =====
+
+The online repository, from which Cygwin packages are downloaded.
+
+Note: although most repositories end with Cygwin32, they are good for 32 and 64 bit Cygwin.
+
+Default value: http://ftp.inf.tu-dresden.de/software/windows/Cygwin32
+
+>>>>> If you are not in Europe, you might want to change this! <<<<<
+
+
+===== -cygcache =====
+
+The local cache folder for Cygwin repositories.
+
+You can also copy files here from a backup/reference and set -cyglocal.
+The setup will then not download/update from the internet but only use the local cache.
+
+Default value: <folder of MakeCoq_MinGW.bat>\Cygwin_cache
+
+
+===== -cyglocal =====
+
+Control if the Cygwin setup uses the latest version from the internet or the version as is in the local folder.
+
+Possible values:
+
+Y: Install exactly the Cygwin version from the local repository cache.
+   Don't update from the internet.
+
+N: Download the latest Cygwin version from the internet.
+   Update the local repository cache with the latest version.
+
+Default value: N
+
+
+===== -cygquiet =====
+
+Control if the Cygwin setup runs quitely or interactive.
+
+Possible values:
+
+Y: Install Cygwin quitely without user interaction.
+
+N: Install Cygwin interactively (allows to select additional packages).
+
+Default value: Y
+
+
+===== -srccache =====
+
+The local cache folder for ocaml/coq/... sources.
+
+Default value: <folder of MakeCoq_MinGW.bat>\source_cache
+
+
+===== -coqver =====
+
+The version of Coq to download and compile.
+
+Possible values: 8.4pl6, 8.5pl2, 8.5pl3, git-v8.6 
+                 Others might work, but are untested.
+                 8.4 is only tested in mode=absoloute
+
+Default value: 8.5pl3
+
+If git- is prepended, the Coq sources are loaded from git.
+
+ATTENTION: with default options, the scripts cache source tar balls in two
+places, the <destination>/build/tarballs folder and the <scripts>/source_cache
+folder. If you modified something in git, you need to delete the cached tar ball
+in both places!
+
+===== -gtksrc =====
+
+Control if GTK and its prerequisites are build from sources or if binary MinGW packages from Cygwin are used
+
+Possible values:
+
+Y: Build GTK from sources, takes about 90 minutes extra.
+   This is useful, if you want to debug/fix GTK or library issues.
+
+N: Use prebuilt MinGW libraries from Cygwin
+
+
+===== -threads =====
+
+Control the maximum number of make threads for modules which support parallel make.
+
+Possible values: 1..N. 
+                 Should not be more than 1.5x the number of cores.
+                 Should not be more than available RAM/2GB (e.g. 4 for 8GB)
+
+
+==================== TODO ====================
+
+- Installer doesn't remove OCAMLLIB environment variables (it is in the script, but doesn't seem to work)
+- CoqIDE doesn't find theme files
+- Finish / test mingw_in_Cygwin mode (coqide doesn't start, coqc slow cause of scanning complete share folder)
+- Possibly create/login as specific user to bash (not sure if it makes sense - nead to create additional bash login link then)
+- maybe move share/doc/menhir somehwere else (reduces coqc startup time)
+- Use original installed file list for removing files in uninstaller 
+
+==================== Issues with relocation ====================
+
+Coq and OCaml are built in a specific folder and are not really intended for relocation e.g. by an installer.
+Some absolute paths in config files are patched in coq_new.nsi.
+
+Coq is made fairly relocatable by first configuring it with PREFIX=./ and then PREFIX=<installdir>.
+OCaml is made relocatable mostly by defining the OCAMLLIB environment variable and by patching some files.
+If you have issues with one of the remaining (unpatched) files below, please let me know.
+
+Text files patched by the installer:
+
+./ocamllib/ld.conf
+./etc/findlib.conf:destdir="D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib"
+./etc/findlib.conf:path="D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib"
+
+Text files containing the install folder path after install:
+
+./bin/mkcamlp5:LIB=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5
+./bin/mkcamlp5.opt:LIB=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5
+./libocaml/Makefile.config:PREFIX=D:/bin/coq64_buildtest_reloc_ocaml20
+./libocaml/Makefile.config:LIBDIR=D:/bin/coq64_buildtest_reloc_ocaml20/libocaml
+./libocaml/site-lib/findlib/Makefile.config:OCAML_CORE_BIN=/cygdrive/d/bin/coq64_buildtest_reloc_ocaml20/bin
+./libocaml/site-lib/findlib/Makefile.config:OCAML_SITELIB=D:/bin/coq64_buildtest_reloc_ocaml20\libocaml\site-lib
+./libocaml/site-lib/findlib/Makefile.config:OCAMLFIND_BIN=D:/bin/coq64_buildtest_reloc_ocaml20\bin
+./libocaml/site-lib/findlib/Makefile.config:OCAMLFIND_CONF=D:/bin/coq64_buildtest_reloc_ocaml20\etc\findlib.conf
+./libocaml/topfind:#directory "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib";;
+./libocaml/topfind:  Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";
+./libocaml/topfind:  Topdirs.dir_load Format.err_formatter "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";
+./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib.cma";; *)
+./libocaml/topfind:(* #load "D:\\bin\\coq64_buildtest_reloc_ocaml20\\libocaml\\site-lib/findlib/findlib_top.cma";; *)
+./man/man1/camlp5.1:These files are installed in the directory D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5.
+./man/man1/camlp5.1:D:/bin/coq64_buildtest_reloc_ocaml20/libocaml/camlp5
+
+Binary files containing the build folder path after install:
+
+$ find . -type f -exec grep "Cygwin_coq64_buildtest_reloc_ocaml20" {} /dev/null \;
+Binary file ./bin/coqtop.byte.exe matches
+Binary file ./bin/coqtop.exe matches
+Binary file ./bin/ocamldoc.exe matches
+Binary file ./bin/ocamldoc.opt.exe matches
+Binary file ./libocaml/ocamldoc/odoc_info.a matches
+Binary file ./libocaml/ocamldoc/odoc_info.cma matches
+
+Binary files containing the install folder path after install:
+
+$ find . -type f -exec grep "coq64_buildtest_reloc_ocaml20" {} /dev/null \;
+Binary file ./bin/camlp4.exe matches
+Binary file ./bin/camlp4boot.exe matches
+Binary file ./bin/camlp4o.exe matches
+Binary file ./bin/camlp4o.opt.exe matches
+Binary file ./bin/camlp4of.exe matches
+Binary file ./bin/camlp4of.opt.exe matches
+Binary file ./bin/camlp4oof.exe matches
+Binary file ./bin/camlp4oof.opt.exe matches
+Binary file ./bin/camlp4orf.exe matches
+Binary file ./bin/camlp4orf.opt.exe matches
+Binary file ./bin/camlp4r.exe matches
+Binary file ./bin/camlp4r.opt.exe matches
+Binary file ./bin/camlp4rf.exe matches
+Binary file ./bin/camlp4rf.opt.exe matches
+Binary file ./bin/camlp5.exe matches
+Binary file ./bin/camlp5o.exe matches
+Binary file ./bin/camlp5o.opt matches
+Binary file ./bin/camlp5r.exe matches
+Binary file ./bin/camlp5r.opt matches
+Binary file ./bin/camlp5sch.exe matches
+Binary file ./bin/coqc.exe matches
+Binary file ./bin/coqchk.exe matches
+Binary file ./bin/coqdep.exe matches
+Binary file ./bin/coqdoc.exe matches
+Binary file ./bin/coqide.exe matches
+Binary file ./bin/coqmktop.exe matches
+Binary file ./bin/coqtop.byte.exe matches
+Binary file ./bin/coqtop.exe matches
+Binary file ./bin/coqworkmgr.exe matches
+Binary file ./bin/coq_makefile.exe matches
+Binary file ./bin/menhir matches
+Binary file ./bin/mkcamlp4.exe matches
+Binary file ./bin/ocaml.exe matches
+Binary file ./bin/ocamlbuild.byte.exe matches
+Binary file ./bin/ocamlbuild.exe matches
+Binary file ./bin/ocamlbuild.native.exe matches
+Binary file ./bin/ocamlc.exe matches
+Binary file ./bin/ocamlc.opt.exe matches
+Binary file ./bin/ocamldebug.exe matches
+Binary file ./bin/ocamldep.exe matches
+Binary file ./bin/ocamldep.opt.exe matches
+Binary file ./bin/ocamldoc.exe matches
+Binary file ./bin/ocamldoc.opt.exe matches
+Binary file ./bin/ocamlfind.exe matches
+Binary file ./bin/ocamlmklib.exe matches
+Binary file ./bin/ocamlmktop.exe matches
+Binary file ./bin/ocamlobjinfo.exe matches
+Binary file ./bin/ocamlopt.exe matches
+Binary file ./bin/ocamlopt.opt.exe matches
+Binary file ./bin/ocamlprof.exe matches
+Binary file ./bin/ocamlrun.exe matches
+Binary file ./bin/ocpp5.exe matches
+Binary file ./lib/config/coq_config.cmo matches
+Binary file ./lib/config/coq_config.o matches
+Binary file ./lib/grammar/grammar.cma matches
+Binary file ./lib/ide/ide_win32_stubs.o matches
+Binary file ./lib/lib/clib.a matches
+Binary file ./lib/lib/clib.cma matches
+Binary file ./lib/libcoqrun.a matches
+Binary file ./libocaml/camlp4/camlp4fulllib.a matches
+Binary file ./libocaml/camlp4/camlp4fulllib.cma matches
+Binary file ./libocaml/camlp4/camlp4lib.a matches
+Binary file ./libocaml/camlp4/camlp4lib.cma matches
+Binary file ./libocaml/camlp4/camlp4o.cma matches
+Binary file ./libocaml/camlp4/camlp4of.cma matches
+Binary file ./libocaml/camlp4/camlp4oof.cma matches
+Binary file ./libocaml/camlp4/camlp4orf.cma matches
+Binary file ./libocaml/camlp4/camlp4r.cma matches
+Binary file ./libocaml/camlp4/camlp4rf.cma matches
+Binary file ./libocaml/camlp5/odyl.cma matches
+Binary file ./libocaml/compiler-libs/ocamlcommon.a matches
+Binary file ./libocaml/compiler-libs/ocamlcommon.cma matches
+Binary file ./libocaml/dynlink.cma matches
+Binary file ./libocaml/expunge.exe matches
+Binary file ./libocaml/extract_crc.exe matches
+Binary file ./libocaml/libcamlrun.a matches
+Binary file ./libocaml/ocamlbuild/ocamlbuildlib.a matches
+Binary file ./libocaml/ocamlbuild/ocamlbuildlib.cma matches
+Binary file ./libocaml/ocamldoc/odoc_info.a matches
+Binary file ./libocaml/ocamldoc/odoc_info.cma matches
+Binary file ./libocaml/site-lib/findlib/findlib.a matches
+Binary file ./libocaml/site-lib/findlib/findlib.cma matches
+Binary file ./libocaml/site-lib/findlib/findlib.cmxs matches
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
new file mode 100644
index 000000000..09a9cf35a
--- /dev/null
+++ b/dev/build/windows/configure_profile.sh
@@ -0,0 +1,32 @@
+#!/bin/bash
+
+rcfile=~/.bash_profile
+donefile=~/.bash_profile.upated
+
+if [ ! -f $donefile ] ; then
+
+    echo >> $rcfile
+    
+    if [ -n "$1" ]; then
+      echo export http_proxy="http://$1" >> $rcfile
+      echo export https_proxy="http://$1" >> $rcfile
+      echo export ftp_proxy="http://$1" >> $rcfile
+    fi
+    
+    mkdir -p $RESULT_INSTALLDIR_CFMT/bin
+
+    # A tightly controlled path helps to avoid issues
+    # Note: the order is important: first have the cygwin binaries, then the mingw binaries in the path!
+    # Note: /bin is mounted at /usr/bin and /lib at /usr/lib and it is common to use /usr/bin in PATH
+    # See cat /proc/mounts
+    echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows" >> $rcfile
+
+    # find and xargs complain if the environment is larger than (I think) 8k.
+    # ORIGINAL_PATH (set by cygwin) can be a few k and exceed the limit
+    echo unset ORIGINAL_PATH >> $rcfile
+    
+    # Other installations of OCaml will mess up things
+    echo unset OCAMLLIB >> $rcfile
+
+    touch $donefile
+fi
\ No newline at end of file
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
new file mode 100644
index 000000000..65278d5c9
--- /dev/null
+++ b/dev/build/windows/difftar-folder.sh
@@ -0,0 +1,86 @@
+#!/bin/bash
+
+###################### COPYRIGHT/COPYLEFT ######################
+
+# (C) 2016 Intel Deutschland GmbH
+# Author: Michael Soegtrop
+#
+# Released to the public by Intel under the
+# GNU Lesser General Public License Version 2.1 or later
+# See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+#
+# With very valuable help on building GTK from
+#   https://wiki.gnome.org/Projects/GTK+/Win32/MSVCCompilationOfGTKStack
+#   http://www.gaia-gis.it/spatialite-3.0.0-BETA/mingw64_how_to.html
+
+###################### Script safety and debugging settings ######################
+
+set -o nounset
+
+# Print usage
+
+if [ "$#" -lt 1 ] ; then
+  echo 'Diff a tar (or compressed tar) file with a folder'
+  echo 'difftar-folder.sh <tarfile> [<folder>] [strip]'
+  echo default for folder is .
+  echo default for strip is 0.
+  echo 'strip must be 0 or 1.'
+  exit 1
+fi
+
+# Parse parameters
+
+tarfile=$1
+
+if [ "$#" -ge 2 ] ; then
+  folder=$2
+else
+  folder=.
+fi
+
+if [ "$#" -ge 3 ] ; then
+  strip=$3
+else
+  strip=0
+fi
+
+# Get path prefix if --strip is used
+
+if [ "$strip" -gt 0 ] ; then
+  prefix=`tar -t -f $tarfile | head -1`
+else
+  prefix=
+fi
+
+# Original folder
+
+if [ "$strip" -gt 0 ] ; then
+  orig=${prefix%/}.orig
+elif [ "$folder" = "." ] ; then
+  orig=${tarfile##*/}
+  orig=./${orig%%.tar*}.orig
+elif [ "$folder" = "" ] ; then
+  orig=${tarfile##*/}
+  orig=${orig%%.tar*}.orig
+else
+  orig=$folder.orig
+fi
+echo $orig
+mkdir -p "$orig"
+
+
+# Make sure tar uses english output (for Mod time differs)
+export LC_ALL=C
+
+# Search all files with a deviating modification time using tar --diff
+tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod time differs" | while read -r file ; do
+  # Substitute ': Mod time differs' with nothing
+  file=${file/: Mod time differs/}
+  # Check if file exists
+  if [ -f "$folder/$file" ] ; then 
+    # Extract original file
+    tar -x -a -f "$tarfile" --strip $strip --directory "$orig" "$prefix$file"
+    # Compute diff
+    diff -u "$orig/$file" "$folder/$file" 
+  fi
+done
\ No newline at end of file
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
new file mode 100644
index 000000000..52b158871
--- /dev/null
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -0,0 +1,1270 @@
+#!/bin/bash
+
+###################### COPYRIGHT/COPYLEFT ######################
+
+# (C) 2016 Intel Deutschland GmbH
+# Author: Michael Soegtrop
+#
+# Released to the public by Intel under the
+# GNU Lesser General Public License Version 2.1 or later
+# See https://www.gnu.org/licenses/old-licenses/lgpl-2.1.html
+#
+# With very valuable help on building GTK from
+#   https://wiki.gnome.org/Projects/GTK+/Win32/MSVCCompilationOfGTKStack
+#   http://www.gaia-gis.it/spatialite-3.0.0-BETA/mingw64_how_to.html
+
+###################### Script safety and debugging settings ######################
+
+set -o nounset
+set -o errexit
+set -x
+
+# Set this to 1 if all module directories shall be removed before build (no incremental make)
+RMDIR_BEFORE_BUILD=1
+
+###################### NOTES #####################
+
+# - This file goes together with MakeCoq_ForMignGW.bat, which sets up cygwin
+#   with all required packages and then calls this script.
+#
+# - This script uses set -o errexit, so if anything fails, the script will stop
+#
+# - cygwin provided mingw64 packages like mingw64-x86_64-zlib are installed to
+#   /usr/$TARGET_ARCH/sys-root/mingw, so we use this as install prefix
+#
+# - if mingw64-x86_64-pkg-config is installed BEFORE building libpng or pixman,
+#   the .pc files are properly created in /usr/$TARGET_ARCH/sys-root/mingw/lib/pkgconfig
+#
+# - pango and some others uses pkg-config executable names without path, which doesn't work in cross compile mode
+#   There are several possible solutions
+#     1.) patch build files to get the prefix from pkg-config and use $prefix/bin/ as path
+#         - doesn't work for pango because automake goes wild
+#         - mingw tools are not able to handle cygwin path (they need absolute windows paths)
+#     2.) export PATH=$PATH:/usr/$TARGET_ARCH/sys-root/mingw/bin
+#         - a bit dangerous because this exposes much more than required
+#         - mingw tools are not able to handle cygwin path (they need absolute windows paths)
+#     3.) Install required tools via cygwin modules libglib2.0-devel and libgdk_pixbuf2.0-devel
+#         - Possibly version compatibility issues
+#         - Possibly mingw/cygwin compatibility issues, e.g. when building font or terminfo databases
+#     4.) Build required tools for mingw and cygwin
+#         - Possibly mingw/cygwin compatibility issues, e.g. when building font or terminfo databases
+#
+#   We use method 3 below
+#   Method 2 can be tried by putting the cross tools in the path before the cygwin tools (in configure_profile.sh)
+#
+# - It is tricky to build 64 bit binaries with 32 bit cross tools and vice versa.
+#   This is because the linker needs to load DLLs from C:\windows\system32, which contains
+#   both 32 bit and 64 bit DLLs, and which one you get depends by some black magic on if the using
+#   app is a 32 bit or 64 bit app. So better build 32 bit mingw with 32 bit cygwin and 64 with 64.
+#   Alternatively the required 32 bit or 64 bit DLLs need to be copied with a 32 bit/64bit cp to some
+#   folder without such black magic.
+#
+# - The file selection for the Coq Windows Installer is done with make install (unlike the original script)
+#   Relocatble builds are first configured with prefix=./ then build and then
+#   reconfigured with prefix=<installroot> before make install.
+
+
+###################### ARCHITECTURES #####################
+
+# The OS on which the build of the tool/lib runs
+BUILD=`gcc -dumpmachine`
+
+# The OS on which the tool runs
+# "`find /bin -name "*mingw32-gcc.exe"`" -dumpmachine
+HOST=$TARGET_ARCH
+
+# The OS for which the tool creates code/for which the libs are
+TARGET=$TARGET_ARCH
+
+# Cygwin uses different arch name for 32 bit than mingw/gcc
+case $ARCH in
+  x86_64) CYGWINARCH=x86_64 ;;
+  i686)   CYGWINARCH=x86 ;;
+  *)      false ;;
+esac
+
+###################### PATHS #####################
+
+# Name and create some 'global' folders
+PATCHES=/build/patches
+BUILDLOGS=/build/buildlogs
+FLAGFILES=/build/flagfiles
+TARBALLS=/build/tarballs
+FILELISTS=/build/filelists
+
+mkdir -p $BUILDLOGS
+mkdir -p $FLAGFILES
+mkdir -p $TARBALLS
+mkdir -p $FILELISTS
+cd /build
+
+
+# sysroot prefix for the above /build/host/target combination
+PREFIX=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw
+
+# Install / Prefix folder for COQ
+PREFIXCOQ=$RESULT_INSTALLDIR_MFMT
+
+# Install / Prefix folder for OCaml
+if [ "$INSTALLOCAML" == "Y" ]; then
+  PREFIXOCAML=$PREFIXCOQ
+else
+  PREFIXOCAML=$PREFIX
+fi
+
+mkdir -p $PREFIX/bin
+mkdir -p $PREFIXCOQ/bin
+mkdir -p $PREFIXOCAML/bin
+
+###################### Copy Cygwin Setup Info #####################
+
+# Copy Cygwin repo ini file and installed files db to tarballs folder.
+# Both files together document the exact selection and version of cygwin packages.
+# Do this as early as possible to avoid changes by other setups (the repo folder is shared).
+
+# Escape URL to folder name
+CYGWIN_REPO_FOLDER=${CYGWIN_REPOSITORY}/
+CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//:/%3a}
+CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//\//%2f}
+
+# Copy files
+cp $CYGWIN_LOCAL_CACHE_WFMT/$CYGWIN_REPO_FOLDER/$CYGWINARCH/setup.ini $TARBALLS
+cp /etc/setup/installed.db $TARBALLS
+  
+###################### LOGGING #####################
+
+# The folder which receives log files
+mkdir -p buildlogs
+LOGS=`pwd`/buildlogs
+
+# The current log target (first part of the log file name)
+LOGTARGET=other
+
+log1() {
+  "$@" > $LOGS/$LOGTARGET-$1.log 2> $LOGS/$LOGTARGET-$1.err
+}
+
+log2() {
+  "$@" > $LOGS/$LOGTARGET-$1-$2.log 2> $LOGS/$LOGTARGET-$1-$2.err
+}
+
+log_1_3() {
+  "$@" > $LOGS/$LOGTARGET-$1-$3.log 2> $LOGS/$LOGTARGET-$1-$3.err
+}
+
+logn() {
+  LOGTARGETEX=$1
+  shift
+  "$@" > $LOGS/$LOGTARGET-$LOGTARGETEX.log 2> $LOGS/$LOGTARGET-$LOGTARGETEX.err
+}
+ 
+###################### UTILITY FUNCTIONS #####################
+
+# ------------------------------------------------------------------------------
+# Get a source tar ball, expand and patch it
+# - get source archive from $SOURCE_LOCAL_CACHE_CFMT or online using wget
+# - create build folder
+# - extract source archive
+# - patch source file if patch exists
+# 
+# Parameters
+# $1 file server name including protocol prefix
+# $2 file name (without extension)
+# $3 file extension
+# $4 number of path levels to strip from tar (usually 1)
+# $5 module name (if different from archive)
+# $6 expand folder name (if different from module name)
+# ------------------------------------------------------------------------------
+
+function get_expand_source_tar {
+  # Handle optional parameters
+  if [ "$#" -ge 4 ] ; then
+    strip=$4
+  else
+    strip=1
+  fi
+
+  if [ "$#" -ge 5 ] ; then
+    name=$5
+  else
+    name=$2
+  fi
+  
+  if [ "$#" -ge 6 ] ; then
+    folder=$6
+  else
+    folder=$name
+  fi
+  
+  # Set logging target
+  logtargetold=$LOGTARGET
+  LOGTARGET=$name
+  
+  # Get the source archive either from the source cache or online
+  if [ ! -f $TARBALLS/$name.$3 ] ; then
+    if [ -f $SOURCE_LOCAL_CACHE_CFMT/$name.$3 ] ; then
+      cp $SOURCE_LOCAL_CACHE_CFMT/$name.$3 $TARBALLS
+    else
+      wget $1/$2.$3
+      if [ ! "$2.$3" == "$name.$3" ] ; then
+        mv $2.$3 $name.$3
+      fi
+      mv $name.$3 $TARBALLS
+      # Save the source archive in the source cache
+      if [ -d $SOURCE_LOCAL_CACHE_CFMT ] ; then
+        cp $TARBALLS/$name.$3 $SOURCE_LOCAL_CACHE_CFMT
+      fi
+    fi
+  fi
+  
+  # Remove build directory (clean build)
+  if [ $RMDIR_BEFORE_BUILD -eq 1 ] ; then
+    rm -f -r $folder
+  fi
+  
+  # Create build directory and cd
+  mkdir -p $folder
+  cd $folder
+  
+  # Extract source archive
+  if [ "$3" == "zip" ] ; then
+    log1 unzip $TARBALLS/$name.$3
+    if [ "$strip" == "1" ] ; then
+      # Ok, this is dirty, but it works and it fails if there are name clashes
+      mv */* .
+    else
+      echo "Unzip strip count not supported"
+      return 1
+    fi
+  else
+    logn untar tar xvaf $TARBALLS/$name.$3 --strip $strip
+  fi
+  
+  # Patch if patch file exists
+  if [ -f $PATCHES/$name.patch ] ; then
+    log1 patch -p1 -i $PATCHES/$name.patch
+  fi
+  
+  # Go back to base folder
+  cd ..
+
+  LOGTARGET=$logtargetold
+}
+
+# ------------------------------------------------------------------------------
+# Prepare a module build
+# - check if build is already done (name.finished file exists) - if so return 1
+# - create name.started
+# - get source archive from $SOURCE_LOCAL_CACHE_CFMT or online using wget
+# - create build folder
+# - cd to build folder and extract source archive
+# - create bin_special subfolder and add it to $PATH
+# - remember things for build_post
+# 
+# Parameters
+# $1 file server name including protocol prefix
+# $2 file name (without extension)
+# $3 file extension
+# $4 [optional] number of path levels to strip from tar (usually 1)
+# $5 [optional] module name (if different from archive)
+# ------------------------------------------------------------------------------
+
+function build_prep {
+  # Handle optional parameters
+  if [ "$#" -ge 4 ] ; then
+    strip=$4
+  else
+    strip=1
+  fi
+
+  if [ "$#" -ge 5 ] ; then
+    name=$5
+  else
+    name=$2
+  fi
+  
+  # Check if build is already done
+  if [ ! -f flagfiles/$name.finished ] ; then
+    BUILD_PACKAGE_NAME=$name
+    BUILD_OLDPATH=$PATH
+    BUILD_OLDPWD=`pwd`
+    LOGTARGET=$name
+
+    touch flagfiles/$name.started
+    
+    get_expand_source_tar $1 $2 $3 $strip $name
+    
+    cd $name
+    
+    # Create a folder and add it to path, where we can put special binaries
+    # The path is restored in build_post
+    mkdir bin_special
+    PATH=`pwd`/bin_special:$PATH
+    
+    return 0
+  else  
+    return 1
+  fi
+}
+
+# ------------------------------------------------------------------------------
+# Finalize a module build
+# - create name.finished
+# - go back to base folder
+# ------------------------------------------------------------------------------
+
+function build_post {
+  if [ ! -f flagfiles/$BUILD_PACKAGE_NAME.finished ]; then
+    cd $BUILD_OLDPWD
+    touch flagfiles/$BUILD_PACKAGE_NAME.finished
+    PATH=$BUILD_OLDPATH
+    LOGTARGET=other
+  fi
+}
+
+# ------------------------------------------------------------------------------
+# Build and install a module using the standard configure/make/make install process
+# - prepare build (as above)
+# - configure
+# - make
+# - make install
+# - finalize build (as above)
+#
+# parameters
+# $1 file server name including protocol prefix
+# $2 file name (without extension)
+# $3 file extension
+# $4 patch function to call between untar and configure (or true if none)
+# $5.. extra configure arguments
+# ------------------------------------------------------------------------------
+
+function build_conf_make_inst {
+  if build_prep $1 $2 $3 ; then
+    $4
+    logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIX "${@:5}"
+    log1 make $MAKE_OPT
+    log2 make install
+    log2 make clean
+    build_post
+  fi
+}
+
+# ------------------------------------------------------------------------------
+# Install all files given by a glob pattern to a given folder
+#
+# parameters
+# $1 glob pattern (in '')
+# $2 target folder
+# ------------------------------------------------------------------------------
+
+function install_glob {
+  # Check if any files matching the pattern exist
+  if [ "$(echo $1)" != "$1" ] ; then
+    install -D -t $2 $1
+  fi
+}
+
+
+# ------------------------------------------------------------------------------
+# Recursively Install all files given by a glob pattern to a given folder
+#
+# parameters
+# $1 source path
+# $2 pattern (in '')
+# $3 target folder
+# ------------------------------------------------------------------------------
+
+function install_rec {
+  ( cd $1 && find -type f -name "$2" -exec install -D -T  $1/{} $3/{} \; )
+}
+
+# ------------------------------------------------------------------------------
+# Write a file list of the target folder
+# The file lists are used to create file lists for the windows installer
+#
+# parameters
+# $1 name of file list
+# ------------------------------------------------------------------------------
+
+function list_files {
+  if [ ! -e "/build/filelists/$1" ] ; then
+    ( cd $PREFIXCOQ && find -type f | sort > /build/filelists/$1 )
+  fi
+}
+
+# ------------------------------------------------------------------------------
+# Compute the set difference of two file lists
+#
+# parameters
+# $1 name of list A-B (set difference of set A minus set B)
+# $2 name of list A
+# $3 name of list B
+# ------------------------------------------------------------------------------
+
+function diff_files {
+  # See http://www.catonmat.net/blog/set-operations-in-unix-shell/ for file list set operations
+  comm -23 <(sort "/build/filelists/$2") <(sort "/build/filelists/$3") > "/build/filelists/$1"
+}
+
+# ------------------------------------------------------------------------------
+# Filter a list of files with a regular expression
+#
+# parameters
+# $1 name of output file list
+# $2 name of input file list
+# $3 name of filter regexp
+# ------------------------------------------------------------------------------
+
+function filter_files {
+  egrep "$3" "/build/filelists/$2" > "/build/filelists/$1"
+}
+
+# ------------------------------------------------------------------------------
+# Convert a file list to NSIS installer format
+#
+# parameters
+# $1 name of file list file (output file is the same with extension .nsi)
+# ------------------------------------------------------------------------------
+
+function files_to_nsis {
+  # Split the path in the file list into path and filename and create SetOutPath and File instructions
+  # Note: File /oname cannot be used, because it does not create the paths as SetOutPath does
+  # Note: I didn't check if the redundant SetOutPath instructions have a bad impact on installer size or install time
+  cat "/build/filelists/$1" | tr '/' '\\' | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
+}
+
+
+###################### MODULE BUILD FUNCTIONS #####################
+
+##### LIBPNG #####
+
+function make_libpng {
+  build_conf_make_inst  http://prdownloads.sourceforge.net/libpng  libpng-1.6.18  tar.gz  true
+}
+
+##### PIXMAN #####
+
+function make_pixman {
+  build_conf_make_inst  http://cairographics.org/releases  pixman-0.32.8  tar.gz  true
+}
+
+##### FREETYPE #####
+
+function make_freetype {
+  build_conf_make_inst  http://sourceforge.net/projects/freetype/files/freetype2/2.6.1  freetype-2.6.1  tar.bz2  true
+}
+
+##### EXPAT #####
+
+function make_expat {
+  build_conf_make_inst  http://sourceforge.net/projects/expat/files/expat/2.1.0  expat-2.1.0  tar.gz  true
+}
+
+##### FONTCONFIG #####
+
+function make_fontconfig {
+  make_freetype
+  make_expat
+  # CONFIGURE PARAMETERS
+  # build/install fails without --disable-docs 
+  build_conf_make_inst  http://www.freedesktop.org/software/fontconfig/release  fontconfig-2.11.94  tar.gz  true  --disable-docs
+}
+
+##### ICONV #####
+
+function make_libiconv {
+  build_conf_make_inst  http://ftp.gnu.org/pub/gnu/libiconv  libiconv-1.14  tar.gz  true
+}
+
+##### UNISTRING #####
+
+function make_libunistring {
+  build_conf_make_inst  http://ftp.gnu.org/gnu/libunistring  libunistring-0.9.5  tar.xz  true
+}
+
+##### NCURSES #####
+
+function make_ncurses {
+  # NOTE: ncurses is not required below. This is just kept for documentary purposes in case I need it later.
+  #
+  # NOTE: make install fails building the terminfo database because
+  # : ${TIC_PATH:=unknown} in run_tic.sh
+  # As a result pkg-config .pc files are not generated
+  # Also configure of gettext gives two "considers"
+  # checking where terminfo library functions come from... not found, consider installing GNU ncurses
+  # checking where termcap library functions come from... not found, consider installing GNU ncurses
+  # gettext make/make install work anyway
+  #
+  # CONFIGURE PARAMETERS
+  # --enable-term-driver --enable-sp-funcs is rewuired for mingw (see README.MinGW)
+  # additional changes 
+  # ADD --with-pkg-config
+  # ADD --enable-pc-files
+  # ADD --without-manpages
+  # REM --with-pthread
+  build_conf_make_inst  http://ftp.gnu.org/gnu/ncurses  ncurses-5.9  tar.gz  true  --disable-home-terminfo --enable-reentrant --enable-sp-funcs --enable-term-driver --enable-interop --with-pkg-config --enable-pc-files --without-manpages
+}
+
+##### GETTEXT #####
+
+function make_gettext {
+  # Cygwin packet dependencies: (not 100% sure) libiconv-devel,libunistring-devel,libncurses-devel
+  # Cygwin packet dependencies for gettext users: (not 100% sure) gettext-devel,libgettextpo-devel
+  # gettext configure complains that ncurses is also required, but it builds without it
+  # Ncurses is tricky to install/configure for mingw64, so I dropped ncurses
+  make_libiconv
+  make_libunistring
+  build_conf_make_inst  http://ftp.gnu.org/pub/gnu/gettext  gettext-0.19  tar.gz  true
+}
+
+##### LIBFFI #####
+
+function make_libffi {
+  # NOTE: The official download server is down  ftp://sourceware.org/pub/libffi/libffi-3.2.1.tar.gz
+  build_conf_make_inst  http://www.mirrorservice.org/sites/sourceware.org/pub/libffi  libffi-3.2.1  tar.gz  true
+}
+
+##### LIBEPOXY #####
+
+function make_libepoxy {
+  build_conf_make_inst  https://github.com/anholt/libepoxy/releases/download/v1.3.1  libepoxy-1.3.1  tar.bz2  true
+}
+
+##### LIBPCRE #####
+
+function make_libpcre {
+  build_conf_make_inst  ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre  pcre-8.39    tar.bz2  true
+}
+
+function make_libpcre2 {
+  build_conf_make_inst  ftp://ftp.csx.cam.ac.uk/pub/software/programming/pcre  pcre2-10.22  tar.bz2  true
+}
+
+##### GLIB #####
+
+function make_glib {
+  # Cygwin packet dependencies: mingw64-x86_64-zlib
+  make_gettext
+  make_libffi
+  make_libpcre
+  # build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/glib/2.46  glib-2.46.0  tar.xz  true
+  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/glib/2.47  glib-2.47.5  tar.xz  true
+}
+
+##### ATK #####
+
+function make_atk {
+  make_gettext
+  make_glib
+  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/atk/2.18  atk-2.18.0  tar.xz  true
+}
+
+##### PIXBUF #####
+
+function make_gdk-pixbuf {
+  # Cygwin packet dependencies: mingw64-x86_64-zlib
+  make_libpng
+  make_gettext
+  make_glib
+  # CONFIGURE PARAMETERS
+  # --with-included-loaders=yes statically links the image file format handlers
+  # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory"
+  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32  gdk-pixbuf-2.32.1  tar.xz  true  --with-included-loaders=yes 
+}
+
+##### CAIRO #####
+
+function make_cairo {
+  # Cygwin packet dependencies: mingw64-x86_64-zlib
+  make_libpng
+  make_glib
+  make_pixman
+  make_fontconfig
+  build_conf_make_inst  http://cairographics.org/releases  cairo-1.14.2  tar.xz  true
+}
+
+##### PANGO #####
+
+function make_pango {
+  make_cairo
+  make_glib
+  make_fontconfig
+  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/pango/1.38  pango-1.38.0  tar.xz  true
+}
+
+##### GTK2 #####
+
+function patch_gtk2 {
+  rm gtk/gtk.def
+}
+
+function make_gtk2 {
+  # Cygwin packet dependencies: gtk-update-icon-cache
+  if [ "$GTK_FROM_SOURCES" == "Y" ]; then
+    make_glib
+    make_atk
+    make_pango
+    make_gdk-pixbuf
+    make_cairo
+    build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/2.24  gtk+-2.24.28  tar.xz  patch_gtk2
+  fi
+}
+
+##### GTK3 #####
+
+function make_gtk3 {
+  make_glib
+  make_atk
+  make_pango
+  make_gdk-pixbuf
+  make_cairo
+  make_libepoxy
+  build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/3.16  gtk+-3.16.7  tar.xz  true
+
+  # make all incl. tests and examples runs through fine
+  # make install fails with issue with 
+  # 
+  # make[5]: Entering directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo'
+  # test -n "" || ../../gtk/gtk-update-icon-cache --ignore-theme-index --force "/usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor"
+  # gtk-update-icon-cache.exe: Failed to open file /usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor/.icon-theme.cache : No such file or directory
+  # Makefile:1373: recipe for target 'install-update-icon-cache' failed
+  # make[5]: *** [install-update-icon-cache] Error 1
+  # make[5]: Leaving directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo'
+}
+
+##### LIBXML2 #####
+
+function make_libxml2 {
+  # Cygwin packet dependencies: libtool automake
+  # Note: latest release version 2.9.2 fails during configuring lzma, so using 2.9.1
+  # Note: python binding requires <sys/select.h> which doesn't exist on cygwin
+  if build_prep https://git.gnome.org/browse/libxml2/snapshot  libxml2-2.9.1  tar.xz ; then
+    # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIX --disable-shared --without-python
+    # shared library required by gtksourceview
+    ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIX --without-python
+    log1 make $MAKE_OPT all
+    log2 make install
+    log2 make clean
+    build_post
+  fi
+}
+
+##### GTK-SOURCEVIEW2 #####
+
+function make_gtk_sourceview2 {
+  # Cygwin packet dependencies: intltool
+  # gtksourceview-2.11.2 requires GTK2
+  # gtksourceview-2.91.9 requires GTK3
+  # => We use gtksourceview-2.11.2 which seems to be the newest GTK2 based one
+  if [ "$GTK_FROM_SOURCES" == "Y" ]; then
+    make_gtk2
+    make_libxml2
+    build_conf_make_inst  https://download.gnome.org/sources/gtksourceview/2.11  gtksourceview-2.11.2  tar.bz2  true
+  fi
+}
+
+##### FLEXDLL FLEXLINK #####
+
+# Note: there is a circular dependency between flexlink and ocaml (resolved in Ocaml 4.03.)
+# For MinGW it is not even possible to first build an Ocaml without flexlink support,
+# Because Makefile.nt doesn't support this. So we have to use a binary flexlink.
+# One could of cause do a bootstrap run ...
+
+# Install flexdll objects
+
+function install_flexdll {
+  cp flexdll.h /usr/$TARGET_ARCH/sys-root/mingw/include
+  if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
+    cp flexdll*_mingw.o /usr/$TARGET_ARCH/bin
+    cp flexdll*_mingw.o $PREFIXOCAML/bin
+  elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
+    cp flexdll*_mingw64.o /usr/$TARGET_ARCH/bin
+    cp flexdll*_mingw64.o $PREFIXOCAML/bin
+  else
+    echo "Unknown target architecture"
+    return 1
+  fi
+}
+
+# Install flexlink
+
+function install_flexlink {
+  cp flexlink.exe /usr/$TARGET_ARCH/bin
+    
+  cp flexlink.exe $PREFIXOCAML/bin
+}
+
+# Get binary flexdll flexlink for building OCaml
+# An alternative is to first build an OCaml without shared library support and build flexlink with it
+
+function get_flex_dll_link_bin {
+  if build_prep http://alain.frisch.fr/flexdll flexdll-bin-0.34 zip 1 ; then
+    install_flexdll
+    install_flexlink
+    build_post
+  fi
+}
+
+# Build flexdll and flexlink from sources after building OCaml
+
+function make_flex_dll_link {
+  if build_prep http://alain.frisch.fr/flexdll flexdll-0.34 tar.gz ; then
+    if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
+      log1 make $MAKE_OPT build_mingw flexlink.exe
+    elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
+      log1 make $MAKE_OPT build_mingw64 flexlink.exe
+    else
+      echo "Unknown target architecture"
+      return 1
+    fi
+    install_flexdll
+    install_flexlink
+    log2 make clean
+    build_post
+  fi
+}
+
+##### LN replacement #####
+
+# Note: this does support symlinks, but symlinks require special user rights on Windows.
+# ocamlbuild uses symlinks to link the executables in the build folder to the base folder.
+# For this purpose hard links are better.
+
+function make_ln {
+  if [ ! -f flagfiles/myln.finished ] ; then
+    touch flagfiles/myln.started
+    mkdir -p myln
+    cd myln
+    cp $PATCHES/ln.c .
+    $TARGET_ARCH-gcc -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c 
+    install -D ln.exe $PREFIXCOQ/bin/ln.exe
+    cd ..
+    touch flagfiles/myln.finished
+  fi
+}
+
+##### OCAML #####
+
+function make_ocaml {
+  get_flex_dll_link_bin
+  if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.02 ocaml-4.02.3 tar.gz 1 ; then
+  # if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.01 ocaml-4.01.0 tar.gz 1 ; then
+    # See README.win32
+    cp config/m-nt.h config/m.h
+    cp config/s-nt.h config/s.h
+    if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
+        cp config/Makefile.mingw config/Makefile
+    elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
+        cp config/Makefile.mingw64 config/Makefile
+    else
+        echo "Unknown target architecture"
+        return 1
+    fi
+
+    # Prefix is fixed in make file - replace it with the real one
+    sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile
+    
+    # We don't want to mess up Coq's dirctory structure so put the OCaml library in a separate folder
+    # If we refer to the make variable ${PREFIX} below, camlp4 ends up having a wrong path:
+    # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
+    # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
+    # So we put an explicit path in there
+    sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile
+    
+    # Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT
+    # I verified that 4.02.3 still doesn't support parallel build
+    log2 make world -f Makefile.nt
+    log2 make bootstrap -f Makefile.nt
+    log2 make opt -f Makefile.nt
+    log2 make opt.opt -f Makefile.nt
+    log2 make install -f Makefile.nt
+    # TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development
+    
+    # Move license files and other into into special folder
+    if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
+      mkdir -p $PREFIXOCAML/license_readme/ocaml
+      # 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources.
+      rm -f *.txt
+      cp LICENSE      $PREFIXOCAML/license_readme/ocaml/License.txt
+      cp INSTALL      $PREFIXOCAML/license_readme/ocaml/Install.txt
+      cp README       $PREFIXOCAML/license_readme/ocaml/ReadMe.txt
+      cp README.win32 $PREFIXOCAML/license_readme/ocaml/ReadMeWin32.txt
+      cp VERSION      $PREFIXOCAML/license_readme/ocaml/Version.txt
+      cp Changes      $PREFIXOCAML/license_readme/ocaml/Changes.txt
+    fi
+
+    build_post
+  fi
+  make_flex_dll_link
+}
+
+##### FINDLIB Ocaml library manager #####
+
+function make_findlib {
+  make_ocaml
+  if build_prep http://download.camlcity.org/download findlib-1.5.6 tar.gz 1 ; then
+    ./configure -bindir $PREFIXOCAML\\bin -sitelib $PREFIXOCAML\\libocaml\\site-lib -config $PREFIXOCAML\\etc\\findlib.conf
+    # Note: findlib doesn't support -j 8, so don't pass MAKE_OPT
+    log2 make all
+    log2 make opt
+    log2 make install
+    log2 make clean
+    build_post
+  fi
+}
+
+##### MENHIR Ocaml Parser Generator #####
+
+function make_menhir {
+  make_ocaml
+  make_findlib
+  # if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20151112 tar.gz 1 ; then
+  # For Ocaml 4.02
+  # if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20151012 tar.gz 1 ; then
+  # For Ocaml 4.01
+  if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20140422 tar.gz 1 ; then
+    # Note: menhir doesn't support -j 8, so don't pass MAKE_OPT
+    log2 make all PREFIX=$PREFIXOCAML
+    log2 make install PREFIX=$PREFIXOCAML
+    mv $PREFIXOCAML/bin/menhir $PREFIXOCAML/bin/menhir.exe
+    build_post
+  fi
+}
+
+##### CAMLP4 Ocaml Preprocessor #####
+
+function make_camlp4 {
+  # OCaml up to 4.01 includes camlp4, from 4.02 it isn't included
+  # Check if command camlp4 exists, if not build camlp4
+  if ! command camlp4 ; then
+    make_ocaml
+    make_findlib
+    if build_prep https://github.com/ocaml/camlp4/archive 4.02+6 tar.gz 1 camlp4-4.02+6 ; then
+      # See https://github.com/ocaml/camlp4/issues/41#issuecomment-112018910
+      logn configure ./configure
+      # Note: camlp4 doesn't support -j 8, so don't pass MAKE_OPT
+      log2 make all
+      log2 make install
+      log2 make clean
+      build_post
+    fi
+  fi
+}
+
+##### CAMLP5 Ocaml Preprocessor #####
+
+function make_camlp5 {
+  make_ocaml
+  make_findlib
+  if build_prep http://camlp5.gforge.inria.fr/distrib/src camlp5-6.14 tgz 1 ; then
+    logn configure ./configure 
+    # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
+    sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
+    log1 make world.opt $MAKE_OPT
+    log2 make install
+    # For some reason gramlib.a is not copied, but it is required by Coq
+    cp lib/gramlib.a $PREFIXOCAML/libocaml/camlp5/
+    log2 make clean
+    build_post
+  fi
+}
+
+##### LABLGTK Ocaml GTK binding #####
+
+# Note: when rebuilding lablgtk by deleting the .finished file,
+# also delete <root>\usr\x86_64-w64-mingw32\sys-root\mingw\lib\site-lib
+# Otherwise make install fails
+
+function make_lablgtk {
+  make_ocaml
+  make_findlib
+  make_camlp4
+  if build_prep https://forge.ocamlcore.org/frs/download.php/1479 lablgtk-2.18.3 tar.gz 1 ; then
+    # configure should be fixed to search for $TARGET_ARCH-pkg-config.exe
+    cp /bin/$TARGET_ARCH-pkg-config.exe  bin_special/pkg-config.exe
+    logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIXOCAML
+    
+    # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
+    
+    # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html for the make || true + strip
+    logn make-world-pre make world || true
+    $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll
+    
+    log2 make world
+    log2 make install
+    log2 make clean
+    build_post
+  fi
+}
+
+##### Ocaml Stdint #####
+
+function make_stdint {
+  make_ocaml
+  make_findlib
+  if build_prep https://github.com/andrenth/ocaml-stdint/archive 0.3.0 tar.gz 1 Stdint-0.3.0; then
+    # Note: the setup gets the proper install path from ocamlfind, but for whatever reason it wants
+    # to create an empty folder in some folder which defaults to C:\Program Files.
+    # The --preifx overrides this. Id didn't see any files created in /tmp/extra.
+    log_1_3 ocaml setup.ml -configure --prefix /tmp/extra
+    log_1_3 ocaml setup.ml -build
+    log_1_3 ocaml setup.ml -install
+    log_1_3 ocaml setup.ml -clean
+    build_post
+  fi
+}
+
+##### COQ #####
+
+# Copy one DLLfrom cygwin MINGW packages to Coq install folder
+
+function copy_coq_dll {
+  if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
+    cp /usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1 $PREFIXCOQ/bin/$1
+  fi
+}
+
+# Copy required DLLs from cygwin MINGW packages to Coq install folder
+
+function copy_coq_dlls {
+  # HOW TO CREATE THE DLL LIST
+  # With the list empty, after the build/install is finished, open coqide in dependency walker.
+  # See http://www.dependencywalker.com/
+  # Make sure to use the 32 bit / 64 bit version of depends matching the target architecture.
+  # Select all missing DLLs from the module list, right click "copy filenames"
+  # Delay loaded DLLs from Windows can be ignored (hour-glass icon at begin of line)
+  # Do this recursively until there are no further missing DLLs (File close + reopen)
+  # For running this quickly, just do "cd coq-<ver> ; call copy_coq_dlls ; cd .." at the end of this script.
+  # Do the same for coqc and ocamlc (usually doesn't result in additional files)
+  
+  copy_coq_dll LIBATK-1.0-0.DLL
+  copy_coq_dll LIBCAIRO-2.DLL
+  copy_coq_dll LIBEXPAT-1.DLL
+  copy_coq_dll LIBFFI-6.DLL
+  copy_coq_dll LIBFONTCONFIG-1.DLL
+  copy_coq_dll LIBFREETYPE-6.DLL
+  copy_coq_dll LIBGDK-WIN32-2.0-0.DLL
+  copy_coq_dll LIBGDK_PIXBUF-2.0-0.DLL
+  copy_coq_dll LIBGIO-2.0-0.DLL
+  copy_coq_dll LIBGLIB-2.0-0.DLL
+  copy_coq_dll LIBGMODULE-2.0-0.DLL
+  copy_coq_dll LIBGOBJECT-2.0-0.DLL
+  copy_coq_dll LIBGTK-WIN32-2.0-0.DLL
+  copy_coq_dll LIBINTL-8.DLL
+  copy_coq_dll LIBPANGO-1.0-0.DLL
+  copy_coq_dll LIBPANGOCAIRO-1.0-0.DLL
+  copy_coq_dll LIBPANGOWIN32-1.0-0.DLL
+  copy_coq_dll LIBPIXMAN-1-0.DLL
+  copy_coq_dll LIBPNG16-16.DLL
+  copy_coq_dll LIBXML2-2.DLL
+  copy_coq_dll ZLIB1.DLL
+
+  # Depends on if GTK is built from sources  
+  if [ "$GTK_FROM_SOURCES" == "Y" ]; then
+    copy_coq_dll libiconv-2.dll
+    copy_coq_dll libpcre-1.dll
+  else
+    copy_coq_dll ICONV.DLL
+    copy_coq_dll LIBBZ2-1.DLL
+    copy_coq_dll LIBGTKSOURCEVIEW-2.0-0.DLL
+    copy_coq_dll LIBHARFBUZZ-0.DLL
+    copy_coq_dll LIBLZMA-5.DLL
+    copy_coq_dll LIBPANGOFT2-1.0-0.DLL
+  fi;
+
+  # Architecture dependent files
+  case $ARCH in
+    x86_64) copy_coq_dll LIBGCC_S_SEH-1.DLL ;;
+    i686)   copy_coq_dll LIBGCC_S_SJLJ-1.DLL ;;
+    *)      false ;;
+  esac
+  
+  # Win pthread version change
+  copy_coq_dll LIBWINPTHREAD-1.DLL
+}
+
+function copy_coq_objects {
+  # copy objects only from folders which exist in the target lib directory
+  find . -type d | while read FOLDER ; do
+    if [ -e $PREFIXCOQ/lib/$FOLDER ] ; then
+      install_glob $FOLDER/'*.cmxa' $PREFIXCOQ/lib/$FOLDER 
+      install_glob $FOLDER/'*.cmi'  $PREFIXCOQ/lib/$FOLDER 
+      install_glob $FOLDER/'*.cma'  $PREFIXCOQ/lib/$FOLDER 
+      install_glob $FOLDER/'*.cmo'  $PREFIXCOQ/lib/$FOLDER 
+      install_glob $FOLDER/'*.a'    $PREFIXCOQ/lib/$FOLDER 
+      install_glob $FOLDER/'*.o'    $PREFIXCOQ/lib/$FOLDER 
+    fi
+  done
+}
+
+# Copy required GTK config and suport files
+
+function copq_coq_gtk {
+  echo 'gtk-theme-name = "MS-Windows"'     >  $PREFIX/etc/gtk-2.0/gtkrc
+  echo 'gtk-fallback-icon-theme = "Tango"' >> $PREFIX/etc/gtk-2.0/gtkrc
+
+  if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
+    install_glob $PREFIX/etc/gtk-2.0/'*'                            $PREFIXCOQ/gtk-2.0
+    install_glob $PREFIX/share/gtksourceview-2.0/language-specs/'*' $PREFIXCOQ/share/gtksourceview-2.0/language-specs
+    install_glob $PREFIX/share/gtksourceview-2.0/styles/'*'         $PREFIXCOQ/share/gtksourceview-2.0/styles
+    install_rec  $PREFIX/share/themes/ '*'                          $PREFIXCOQ/share/themes
+    
+    # This below item look like a bug in make install
+    if [[ ! $COQ_VERSION == 8.4* ]] ; then
+      mv $PREFIXCOQ/share/coq/*.lang $PREFIXCOQ/share/gtksourceview-2.0/language-specs
+      mv $PREFIXCOQ/share/coq/*.xml  $PREFIXCOQ/share/gtksourceview-2.0/styles
+    fi
+    mkdir -p $PREFIXCOQ/ide
+    mv $PREFIXCOQ/share/coq/*.png  $PREFIXCOQ/ide
+    rmdir $PREFIXCOQ/share/coq
+  fi
+}
+
+# Copy license and other info files
+
+function copy_coq_license {
+  if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
+    install -D doc/LICENSE                    $PREFIXCOQ/license_readme/coq/LicenseDoc.txt
+    install -D LICENSE                        $PREFIXCOQ/license_readme/coq/License.txt
+    install -D plugins/micromega/LICENSE.sos  $PREFIXCOQ/license_readme/coq/LicenseMicromega.txt
+    install -D README                         $PREFIXCOQ/license_readme/coq/ReadMe.txt || true
+    install -D README.md                      $PREFIXCOQ/license_readme/coq/ReadMe.md || true
+    install -D README.doc                     $PREFIXCOQ/license_readme/coq/ReadMeDoc.txt
+    install -D CHANGES                        $PREFIXCOQ/license_readme/coq/Changes.txt
+    install -D INSTALL                        $PREFIXCOQ/license_readme/coq/Install.txt
+    install -D INSTALL.doc                    $PREFIXCOQ/license_readme/coq/InstallDoc.txt
+    install -D INSTALL.ide                    $PREFIXCOQ/license_readme/coq/InstallIde.txt
+  fi
+}
+
+# Main function for creating Coq
+
+function make_coq {
+  make_ocaml
+  make_lablgtk
+  make_camlp5
+  if 
+    case $COQ_VERSION in
+      git-*) build_prep https://github.com/coq/coq/archive ${COQ_VERSION##git-} zip 1 coq-${COQ_VERSION} ;;
+      *)     build_prep https://coq.inria.fr/distrib/V$COQ_VERSION/files coq-$COQ_VERSION tar.gz ;;
+    esac
+  then
+    if [ "$INSTALLMODE" == "relocatable" ]; then
+      # HACK: for relocatable builds, first configure with ./, then build but before install reconfigure with the real target path
+      logn configure ./configure -debug -with-doc no -prefix ./ -libdir ./lib -mandir ./man
+    elif [ "$INSTALLMODE" == "absolute" ]; then
+      logn configure ./configure -debug -with-doc no -prefix $PREFIXCOQ -libdir $PREFIXCOQ/lib -mandir $PREFIXCOQ/man
+    else
+      logn configure ./configure -debug -with-doc no -prefix $PREFIXCOQ
+    fi
+
+    # The windows resource compiler binary name is hard coded
+    sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build 
+    sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.ide || true
+
+    # 8.4x doesn't support parallel make
+    if [[ $COQ_VERSION == 8.4* ]] ; then
+      log1 make
+    else
+      log1 make $MAKE_OPT
+    fi
+    
+    if [ "$INSTALLMODE" == "relocatable" ]; then
+      ./configure -debug -with-doc no -prefix $PREFIXCOQ -libdir $PREFIXCOQ/lib -mandir $PREFIXCOQ/man
+    fi
+
+    log2 make install
+    log1 copy_coq_dlls
+    if [ "$INSTALLOCAML" == "Y" ]; then
+      log1 copy_coq_objects
+    fi
+    
+    copq_coq_gtk
+    copy_coq_license
+
+    # make clean seems to br broken for 8.5pl2
+    # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
+    # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
+    # make clean
+    
+    build_post
+  fi
+}
+
+##### GNU Make for MinGW #####
+
+function make_mingw_make {
+  if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then
+    # The config.h.win32 file is fine - don't edit it
+    # We need to copy the mingw gcc here as "gcc" - then the batch file will use it
+    cp /usr/bin/${ARCH}-w64-mingw32-gcc-5.4.0.exe ./gcc.exe
+    # By some magic cygwin bash can run batch files
+    logn build ./build_w32.bat gcc
+    # Copy make to Coq folder
+    cp GccRel/gnumake.exe $PREFIXCOQ/bin/make.exe
+    build_post
+  fi
+}
+
+##### GNU binutils for native OCaml #####
+
+function make_binutils {
+  if build_prep http://ftp.gnu.org/gnu/binutils binutils-2.27 tar.gz ; then
+    logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix=$PREFIXCOQ --program-prefix=$TARGET-
+    log1 make $MAKE_OPT
+    log2 make install
+    # log2 make clean
+    build_post
+  fi
+}
+
+##### GNU GCC for native OCaml #####
+
+function make_gcc {
+  # Note: the bz2 file is smaller, but decompressing bz2 really takes ages
+  if build_prep ftp://ftp.fu-berlin.de/unix/languages/gcc/releases/gcc-5.4.0 gcc-5.4.0 tar.gz ; then
+    # This is equivalent to "contrib/download_prerequisites" but uses caching
+    # Update versions when updating gcc version
+    get_expand_source_tar  ftp://gcc.gnu.org/pub/gcc/infrastructure  mpfr-2.4.2 tar.bz2 1 mpfr-2.4.2 mpfr
+    get_expand_source_tar  ftp://gcc.gnu.org/pub/gcc/infrastructure  gmp-4.3.2  tar.bz2 1 gmp-4.3.2  gmp
+    get_expand_source_tar  ftp://gcc.gnu.org/pub/gcc/infrastructure  mpc-0.8.1  tar.gz  1 mpc-0.8.1  mpc
+    get_expand_source_tar  ftp://gcc.gnu.org/pub/gcc/infrastructure  isl-0.14   tar.bz2 1 isl-0.14   isl
+
+    # For whatever reason gcc needs this (although it never puts anything into it)
+    # Error: "The directory that should contain system headers does not exist:"
+    # mkdir -p /mingw/include    without --with-sysroot
+    mkdir -p $PREFIXCOQ/mingw/include
+
+    # See https://gcc.gnu.org/install/configure.html
+    logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET \
+        --prefix=$PREFIXCOQ --program-prefix=$TARGET- --disable-win32-registry --with-sysroot=$PREFIXCOQ \
+        --enable-languages=c --disable-nls \
+        --disable-libsanitizer --disable-libssp --disable-libquadmath --disable-libgomp --disable-libvtv --disable-lto
+        # --disable-decimal-float seems to be required
+        # --with-sysroot=$PREFIX  results in configure error that this is not an absolute path
+    log1 make $MAKE_OPT
+    log2 make install
+    # log2 make clean
+    build_post
+  fi
+}
+
+##### Get sources for Cygwin MinGW packages #####
+
+function get_cygwin_mingw_sources {
+  if [ ! -f flagfiles/cygwin_mingw_sources.finished ] ; then
+    touch flagfiles/cygwin_mingw_sources.started
+
+    # Find all installed files with mingw in the name and download the corresponding source code file from cygwin
+    # Steps:
+    # grep /etc/setup/installed.db for mingw       => mingw64-x86_64-gcc-g++ mingw64-x86_64-gcc-g++-5.4.0-2.tar.bz2 1
+    # remove archive ending and trailing number    => mingw64-x86_64-gcc-g++ mingw64-x86_64-gcc-g++-5.4.0-2
+    # replace space with /                         => ${ARCHIVE} = mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g++-5.4.0-2
+    # escape + signs using ${var//pattern/replace} => ${ARCHIVEESC} = mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g\+\+-5.4.0-2
+    # grep cygwin setup.ini for installed line + next line (the -A 1 option includes and "after context" of 1 line)
+    # Note that the folders of the installed binaries and source are different. So we cannot grep just for the source line.
+    # We could strip off the path and just grep for the file, though.
+    # => install: x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-g++/mingw64-x86_64-gcc-g++-5.4.0-2.tar.xz 10163848 2f8cb7ba3e16ac8ce0455af01de490ded09061b1b06a9a8e367426635b5a33ce230e04005f059d4ea7b52580757da1f6d5bae88eba6b9da76d1bd95e8844b705
+    #    source: x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz 95565368 03f22997b7173b243fff65ea46a39613a2e4e75fc7e6cf0fa73b7bcb86071e15ba6d0ca29d330c047fb556a5e684cad57cd2f5adb6e794249e4b01fe27f92c95
+    # Take the 2nd field of the last line          => ${SOURCE} = x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
+    # Remove that path part                        => ${SOURCEFILE} = mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
+
+    grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//'  | while read ARCHIVE ; do
+      local ARCHIVEESC=${ARCHIVE//+/\\+}
+      local SOURCE=`egrep -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2`
+      local SOURCEFILE=${SOURCE##*/}
+
+      # Get the source file (either from the source cache or online)
+      if [ ! -f $TARBALLS/$SOURCEFILE ] ; then
+        if [ -f $SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE ] ; then
+          cp $SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE $TARBALLS
+        else
+          wget "$CYGWIN_REPOSITORY/$SOURCE"
+          mv $SOURCEFILE $TARBALLS
+          # Save the source archive in the source cache
+          if [ -d $SOURCE_LOCAL_CACHE_CFMT ] ; then
+            cp $TARBALLS/$SOURCEFILE $SOURCE_LOCAL_CACHE_CFMT
+          fi
+        fi
+      fi
+
+    done
+
+    touch flagfiles/cygwin_mingw_sources.finished
+  fi
+}
+
+##### Coq Windows Installer #####
+
+function make_coq_installer {
+  make_coq
+  make_mingw_make
+  get_cygwin_mingw_sources
+
+  # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build:
+  # ocaml: ocaml + menhir + camlp5 + findlib
+  # ocal_coq: as above + coq
+  
+  # Create coq file list as ocaml_coq / ocaml
+  diff_files coq ocaml_coq ocaml
+  
+  # Filter out object files
+  filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$' 
+  
+  # Filter out plugin object files
+  filter_files coq_objects_plugins coq_objects '/lib/plugins/.*\.(cmxa|cmi|cma|cmo|a|o)$'
+  
+  # Coq objects objects required for plugin development = coq objects except those for pre installed plugins
+  diff_files coq_plugindev coq_objects coq_objects_plugins
+  
+  # Coq files, except objects needed only for plugin development
+  diff_files coq_base coq coq_plugindev
+  
+  # Convert section files to NSIS format
+  files_to_nsis coq_base
+  files_to_nsis coq_plugindev
+  files_to_nsis ocaml
+  
+  # Get and extract NSIS Binaries
+  if build_prep http://downloads.sourceforge.net/project/nsis/NSIS%202/2.51 nsis-2.51 zip ; then
+    NSIS=`pwd`/makensis.exe
+    chmod u+x "$NSIS"
+    # Change to Coq folder
+    cd ../coq-${COQ_VERSION}
+    # Copy patched nsi file
+    cp ../patches/coq_new.nsi dev/nsis
+    cp ../patches/StrRep.nsh dev/nsis
+    cp ../patches/ReplaceInFile.nsh dev/nsis
+    VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
+    cd dev/nsis
+    logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH=$PREFIXCOQ -DCOQ_ICON=..\\..\\ide\\coq.ico coq_new.nsi
+    
+    build_post
+  fi
+}
+
+###################### TOP LEVEL BUILD #####################
+
+make_gtk2
+make_gtk_sourceview2
+
+make_ocaml
+make_findlib
+make_lablgtk
+make_camlp4
+make_camlp5
+make_menhir
+make_stdint
+list_files ocaml
+make_coq
+
+if [ "$INSTALLMAKE" == "Y" ] ; then
+  make_mingw_make
+fi
+
+list_files ocaml_coq
+
+if [ "$MAKEINSTALLER" == "Y" ] ; then
+  make_coq_installer
+fi
+
diff --git a/dev/build/windows/patches_coq/ReplaceInFile.nsh b/dev/build/windows/patches_coq/ReplaceInFile.nsh
new file mode 100644
index 000000000..27c7eb2fd
--- /dev/null
+++ b/dev/build/windows/patches_coq/ReplaceInFile.nsh
@@ -0,0 +1,67 @@
+; From NSIS Wiki http://nsis.sourceforge.net/ReplaceInFile
+; Modifications:
+; - Replace only once per line
+; - Don't keep original as .old
+; - Use StrRep instead of StrReplace (seems to be cleaner)
+
+Function Func_ReplaceInFile
+  ClearErrors
+
+  Exch $0      ; REPLACEMENT
+  Exch
+  Exch $1      ; SEARCH_TEXT
+  Exch 2
+  Exch $2      ; SOURCE_FILE
+
+  Push $R0     ; SOURCE_FILE file handle
+  Push $R1     ; temporary file handle
+  Push $R2     ; unique temporary file name
+  Push $R3     ; a line to search and replace / save
+  Push $R4     ; shift puffer
+
+  IfFileExists $2 +1 error          ; Check if file exists and open it
+  FileOpen $R0 $2 "r"
+
+  GetTempFileName $R2               ; Create temporary output file
+  FileOpen $R1 $R2 "w"
+
+  loop:                             ; Loop over lines of file
+    FileRead $R0 $R3                ; Read line
+    IfErrors finished
+    Push "$R3"                      ; Replacine string in line once
+    Push "$1"
+    Push "$0"
+    Call Func_StrRep
+    Pop $R3
+    FileWrite $R1 "$R3"             ; Write result
+  Goto loop
+
+  finished:
+    FileClose $R1                   ; Close files
+    FileClose $R0
+    Delete "$2"                     ; Delete original file and rename temporary file to target
+    Rename "$R2" "$2"
+    ClearErrors
+    Goto out
+
+  error:
+    SetErrors
+
+  out:
+  Pop $R4
+  Pop $R3
+  Pop $R2
+  Pop $R1
+  Pop $R0
+  Pop $2
+  Pop $0
+  Pop $1
+FunctionEnd
+
+!macro ReplaceInFile SOURCE_FILE SEARCH_TEXT REPLACEMENT
+  Push "${SOURCE_FILE}"
+  Push "${SEARCH_TEXT}"
+  Push "${REPLACEMENT}"
+  Call Func_ReplaceInFile
+!macroend
+
diff --git a/dev/build/windows/patches_coq/StrRep.nsh b/dev/build/windows/patches_coq/StrRep.nsh
new file mode 100644
index 000000000..d94a9f88b
--- /dev/null
+++ b/dev/build/windows/patches_coq/StrRep.nsh
@@ -0,0 +1,60 @@
+; From NSIS Wiki http://nsis.sourceforge.net/StrRep
+; Slightly modified
+
+Function Func_StrRep
+    Exch $R2 ;new
+    Exch 1
+    Exch $R1 ;old
+    Exch 2
+    Exch $R0 ;string
+    Push $R3
+    Push $R4
+    Push $R5
+    Push $R6
+    Push $R7
+    Push $R8
+    Push $R9
+
+    StrCpy $R3 0
+    StrLen $R4 $R1
+    StrLen $R6 $R0
+    StrLen $R9 $R2
+    loop:
+        StrCpy $R5 $R0 $R4 $R3
+        StrCmp $R5 $R1 found
+        StrCmp $R3 $R6 done
+        IntOp $R3 $R3 + 1 ;move offset by 1 to check the next character
+        Goto loop
+    found:
+        StrCpy $R5 $R0 $R3
+        IntOp $R8 $R3 + $R4
+        StrCpy $R7 $R0 "" $R8
+        StrCpy $R0 $R5$R2$R7
+        StrLen $R6 $R0
+        IntOp $R3 $R3 + $R9 ;move offset by length of the replacement string
+        Goto loop
+    done:
+
+    Pop $R9
+    Pop $R8
+    Pop $R7
+    Pop $R6
+    Pop $R5
+    Pop $R4
+    Pop $R3
+    Push $R0
+    Push $R1
+    Pop $R0
+    Pop $R1
+    Pop $R0
+    Pop $R2
+    Exch $R1
+FunctionEnd
+
+!macro StrRep output string old new
+    Push `${string}`
+    Push `${old}`
+    Push `${new}`
+    Call Func_StrRep
+    Pop ${output}
+!macroend
diff --git a/dev/build/windows/patches_coq/camlp4-4.02+6.patch b/dev/build/windows/patches_coq/camlp4-4.02+6.patch
new file mode 100644
index 000000000..0cdb4a929
--- /dev/null
+++ b/dev/build/windows/patches_coq/camlp4-4.02+6.patch
@@ -0,0 +1,11 @@
+--- camlp4-4.02-6.orig/myocamlbuild.ml	2015-06-17 13:37:36.000000000 +0200
++++ camlp4-4.02+6/myocamlbuild.ml	2016-10-13 13:57:35.512213600 +0200
+@@ -86,7 +86,7 @@
+         let dep = "camlp4"/"boot"/exe in
+         let cmd =
+           let ( / ) = Filename.concat in
+-          "camlp4"/"boot"/exe
++          String.escaped (String.escaped ("camlp4"/"boot"/exe))
+         in
+         (Some dep, cmd)
+     in
diff --git a/dev/build/windows/patches_coq/coq-8.4pl2.patch b/dev/build/windows/patches_coq/coq-8.4pl2.patch
new file mode 100644
index 000000000..45a66d0bf
--- /dev/null
+++ b/dev/build/windows/patches_coq/coq-8.4pl2.patch
@@ -0,0 +1,11 @@
+--- configure	2014-04-14 22:28:39.174177924 +0200
++++ configure	2014-04-14 22:29:23.253025166 +0200
+@@ -335,7 +335,7 @@
+   MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3`
+   MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1`
+   MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
+-  if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
++  if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ] || [ "$MAKEVERSIONMAJOR" -ge 4 ] ; then
+       echo "You have GNU Make $MAKEVERSION. Good!"
+   else
+       OK="no"
\ No newline at end of file
diff --git a/dev/build/windows/patches_coq/coq-8.4pl6.patch b/dev/build/windows/patches_coq/coq-8.4pl6.patch
new file mode 100644
index 000000000..c3b7f8574
--- /dev/null
+++ b/dev/build/windows/patches_coq/coq-8.4pl6.patch
@@ -0,0 +1,13 @@
+coq-8.4pl6.orig
+--- coq-8.4pl6.orig/configure	2015-04-09 15:59:35.000000000 +0200
++++ coq-8.4pl6//configure	2016-11-09 13:29:42.235319800 +0100
+@@ -309,9 +309,6 @@
+ # executable extension
+ 
+ case "$ARCH,$CYGWIN" in
+-    win32,yes)
+-      EXE=".exe"
+-      DLLEXT=".so";;
+     win32,*)
+       EXE=".exe"
+       DLLEXT=".dll";;
diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi
new file mode 100644
index 000000000..b88aa066d
--- /dev/null
+++ b/dev/build/windows/patches_coq/coq_new.nsi
@@ -0,0 +1,223 @@
+; This script is used to build the Windows install program for Coq.
+
+; NSIS Modern User Interface
+; Written by Joost Verburg
+; Modified by Julien Narboux, Pierre Letouzey, Enrico Tassi and Michael Soegtrop
+
+; The following command line defines are expected:
+; VERSION      Coq version, e.g. 8.5-pl2
+; ARCH         The target architecture, either x86_64 or i686
+; COQ_SRC_PATH path of Coq installation in Windows or MinGW format (either \\ or /, but with drive letter)
+; COQ_ICON     path of Coq icon file in Windows or MinGW format
+
+; Enable compression after debugging.
+; SetCompress off
+SetCompressor lzma
+
+!define MY_PRODUCT "Coq" ;Define your own software name here
+!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe"
+
+!include "MUI2.nsh"
+!include "FileAssociation.nsh"
+!include "StrRep.nsh"
+!include "ReplaceInFile.nsh"
+!include "winmessages.nsh"
+
+Var COQ_SRC_PATH_BS   ; COQ_SRC_PATH with \ instead of /
+Var COQ_SRC_PATH_DBS  ; COQ_SRC_PATH with \\ instead of /
+Var INSTDIR_DBS       ; INSTDIR with \\ instead of \
+
+;--------------------------------
+;Configuration
+
+  Name "Coq"
+
+  ;General
+  OutFile "${OUTFILE}"
+
+  ;Folder selection page
+  InstallDir "C:\${MY_PRODUCT}"
+  
+  ;Remember install folder
+  InstallDirRegKey HKCU "Software\${MY_PRODUCT}" ""
+
+;--------------------------------
+;Modern UI Configuration
+  
+  !define MUI_ICON "${COQ_ICON}"
+
+  !insertmacro MUI_PAGE_WELCOME
+  !insertmacro MUI_PAGE_LICENSE "${COQ_SRC_PATH}/license_readme/coq/License.txt"
+  !insertmacro MUI_PAGE_COMPONENTS
+  !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where to install Coq.  The path MUST NOT include spaces."
+  !insertmacro MUI_PAGE_DIRECTORY
+  !insertmacro MUI_PAGE_INSTFILES
+  !insertmacro MUI_PAGE_FINISH
+  
+  !insertmacro MUI_UNPAGE_WELCOME
+  !insertmacro MUI_UNPAGE_CONFIRM
+  !insertmacro MUI_UNPAGE_INSTFILES
+  !insertmacro MUI_UNPAGE_FINISH  
+
+;--------------------------------
+;Languages
+ 
+  !insertmacro MUI_LANGUAGE "English"
+  
+;--------------------------------
+;Language Strings
+
+  ;Description
+  LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE."
+  LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development."
+  LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq."
+  LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user."
+  LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users."
+
+;--------------------------------
+; Check for white spaces
+Function .onVerifyInstDir
+  StrLen $0 "$INSTDIR"
+  StrCpy $1 0
+  ${While} $1 < $0
+    StrCpy $3 $INSTDIR 1 $1
+    StrCmp $3 " " SpacesInPath
+    IntOp $1 $1 + 1
+  ${EndWhile}
+  Goto done
+  SpacesInPath:
+  Abort
+  done:
+FunctionEnd
+
+;--------------------------------
+;Installer Sections
+
+
+Section "Coq" Sec1
+
+  SetOutPath "$INSTDIR\"
+  !include "..\..\..\filelists\coq_base.nsh"
+
+  ${registerExtension} "$INSTDIR\bin\coqide.exe" ".v" "Coq Script File"
+
+  ;Store install folder
+  WriteRegStr HKCU "Software\${MY_PRODUCT}" "" $INSTDIR
+  
+  ;Create uninstaller
+  WriteUninstaller "$INSTDIR\Uninstall.exe"
+  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+      "DisplayName" "Coq Version ${VERSION}"
+  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+      "UninstallString" '"$INSTDIR\Uninstall.exe"'
+  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+      "DisplayVersion" "${VERSION}"
+  WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+      "NoModify" "1"
+  WriteRegDWORD HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+      "NoRepair" "1"
+  WriteRegStr HKEY_LOCAL_MACHINE "Software\Microsoft\Windows\CurrentVersion\Uninstall\Coq" \
+      "URLInfoAbout" "http://coq.inria.fr"
+
+  ; Create start menu entries
+  ; SetOutPath is required for the path in the .lnk files
+  SetOutPath "$INSTDIR" 
+  CreateDirectory "$SMPROGRAMS\Coq"
+  ; The first shortcut set here is treated as main application by Windows 7/8.
+  ; Use CoqIDE as main application
+  CreateShortCut "$SMPROGRAMS\Coq\CoqIde.lnk" "$INSTDIR\bin\coqide.exe"
+  CreateShortCut "$SMPROGRAMS\Coq\Coq.lnk" "$INSTDIR\bin\coqtop.exe"
+  WriteINIStr "$SMPROGRAMS\Coq\The Coq HomePage.url" "InternetShortcut" "URL" "http://coq.inria.fr"
+  WriteINIStr "$SMPROGRAMS\Coq\The Coq Standard Library.url" "InternetShortcut" "URL" "http://coq.inria.fr/library"
+  CreateShortCut "$SMPROGRAMS\Coq\Uninstall.lnk" "$INSTDIR\Uninstall.exe" "" "$INSTDIR\Uninstall.exe" 0
+
+SectionEnd
+
+;OCAML Section "Ocaml for native compute and plugin development" Sec2
+;OCAML   SetOutPath "$INSTDIR\"
+;OCAML   !include "..\..\..\filelists\ocaml.nsh"
+;OCAML 
+;OCAML   ; Create a few slash / backslash variants of the source and install path
+;OCAML   ; Note: NSIS has variables, written as $VAR and defines, written as ${VAR}
+;OCAML   !insertmacro StrRep $COQ_SRC_PATH_BS  ${COQ_SRC_PATH} "/" "\"
+;OCAML   !insertmacro StrRep $COQ_SRC_PATH_DBS ${COQ_SRC_PATH} "/" "\\"
+;OCAML   !insertmacro StrRep $INSTDIR_DBS      $INSTDIR        "\" "\\"
+;OCAML 
+;OCAML   ; Replace absolute paths in some OCaml config files
+;OCAML   ; These are not all, see ReadMe.txt
+;OCAML   !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "/"  "\"
+;OCAML   !insertmacro ReplaceInFile "$INSTDIR\libocaml\ld.conf" "$COQ_SRC_PATH_BS"  "$INSTDIR"
+;OCAML   !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS"
+;OCAML SectionEnd
+ 
+Section "Coq files for plugin developers" Sec3
+  SetOutPath "$INSTDIR\"
+  !include "..\..\..\filelists\coq_plugindev.nsh"
+SectionEnd
+
+;OCAML Section "OCAMLLIB current user" Sec4
+;OCAML    WriteRegStr HKCU "Environment" "OCAMLLIB" "$INSTDIR\libocaml"
+;OCAML    ; This is required, so that a newly started shell gets the new environment variable
+;OCAML    ; But it really takes a few seconds
+;OCAML    DetailPrint "Broadcasting OCAMLLIB environment variable change (current user)"
+;OCAML    SendMessage ${HWND_BROADCAST} ${WM_WININICHANGE} 0 "STR:Environment" /TIMEOUT=1000
+;OCAML SectionEnd
+
+;OCAML Section "OCAMLLIB all users" Sec5
+;OCAML    WriteRegStr HKLM "SYSTEM\CurrentControlSet\Control\Session Manager\Environment" "OCAMLLIB" "$INSTDIR\libocaml"
+;OCAML    ; This is required, so that a newly started shell gets the new environment variable
+;OCAML    ; But it really takes a few seconds
+;OCAML    DetailPrint "Broadcasting OCAMLLIB environment variable change (all users)"
+;OCAML    SendMessage ${HWND_BROADCAST} ${WM_WININICHANGE} 0 "STR:Environment" /TIMEOUT=1000
+;OCAML SectionEnd
+
+;--------------------------------
+;Descriptions
+
+!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
+  !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
+  ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
+  !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3)
+  ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4)
+  ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5)
+!insertmacro MUI_FUNCTION_DESCRIPTION_END
+ 
+;--------------------------------
+;Uninstaller Section
+
+Section "Uninstall"
+  ; Files and folders
+  RMDir /r "$INSTDIR\bin"
+  RMDir /r "$INSTDIR\dev"
+  RMDir /r "$INSTDIR\etc"
+  RMDir /r "$INSTDIR\lib"
+  RMDir /r "$INSTDIR\libocaml"
+  RMDir /r "$INSTDIR\share"
+  RMDir /r "$INSTDIR\ide"
+  RMDir /r "$INSTDIR\gtk-2.0"
+  RMDir /r "$INSTDIR\latex"
+  RMDir /r "$INSTDIR\license_readme"
+  RMDir /r "$INSTDIR\man"
+  RMDir /r "$INSTDIR\emacs"
+
+  ; Start Menu
+  Delete "$SMPROGRAMS\Coq\Coq.lnk"
+  Delete "$SMPROGRAMS\Coq\CoqIde.lnk"
+  Delete "$SMPROGRAMS\Coq\Uninstall.lnk"
+  Delete "$SMPROGRAMS\Coq\The Coq HomePage.url"
+  Delete "$SMPROGRAMS\Coq\The Coq Standard Library.url"
+  Delete "$INSTDIR\Uninstall.exe"
+  
+  ; Registry keys
+  DeleteRegKey HKCU "Software\${MY_PRODUCT}"
+  DeleteRegKey HKLM "SOFTWARE\Coq"
+  DeleteRegKey HKLM "SOFTWARE\Microsoft\Windows\CurrentVersion\Uninstall\Coq"
+  DeleteRegKey HKCU "Environment\OCAMLLIB"
+  DeleteRegKey HKLM "SYSTEM\CurrentControlSet\Control\Session Manager\Environment\OCAMLLIB"
+  ${unregisterExtension} ".v" "Coq Script File"
+
+  ; Root folders
+  RMDir "$INSTDIR"
+  RMDir "$SMPROGRAMS\Coq"
+
+SectionEnd
diff --git a/dev/build/windows/patches_coq/flexdll-0.34.patch b/dev/build/windows/patches_coq/flexdll-0.34.patch
new file mode 100644
index 000000000..16389baca
--- /dev/null
+++ b/dev/build/windows/patches_coq/flexdll-0.34.patch
@@ -0,0 +1,14 @@
+reloc.ml
+--- orig.flexdll-0.34/reloc.ml	2015-01-22 17:30:07.000000000 +0100
++++ flexdll-0.34/reloc.ml	2016-10-12 11:59:16.885829700 +0200
+@@ -117,8 +117,8 @@
+ 
+ let new_cmdline () =
+   let rf = match !toolchain with
+-  | `MSVC | `MSVC64 | `LIGHTLD -> true
+-  | `MINGW | `MINGW64 | `GNAT | `CYGWIN | `CYGWIN64 -> false
++  | `MSVC | `MSVC64 | `LIGHTLD | `MINGW | `MINGW64 -> true
++  | `GNAT | `CYGWIN | `CYGWIN64 -> false
+   in
+   {
+    may_use_response_file = rf;
diff --git a/dev/build/windows/patches_coq/glib-2.46.0.patch b/dev/build/windows/patches_coq/glib-2.46.0.patch
new file mode 100644
index 000000000..9082460bf
--- /dev/null
+++ b/dev/build/windows/patches_coq/glib-2.46.0.patch
@@ -0,0 +1,30 @@
+diff -u -r glib-2.46.0/gio/glocalfile.c glib-2.46.0.patched/gio/glocalfile.c
+--- glib-2.46.0/gio/glocalfile.c	2015-08-27 05:32:26.000000000 +0200
++++ glib-2.46.0.patched/gio/glocalfile.c	2016-01-27 13:08:30.059736400 +0100
+@@ -2682,7 +2682,10 @@
+         (!g_path_is_absolute (filename) || len > g_path_skip_root (filename) - filename))
+       wfilename[len] = '\0';
+ 
+-    retval = _wstat32i64 (wfilename, &buf);
++    // MSoegtrop: _wstat32i64 is the wrong function for GLocalFileStat = struct _stati64
++    // The correct function is _wstati64, see https://msdn.microsoft.com/en-us/library/14h5k7ff.aspx
++    // Also _wstat32i64 is a VC function, not a windows SDK function, see https://msdn.microsoft.com/en-us/library/aa273365(v=vs.60).aspx
++    retval = _wstati64 (wfilename, &buf);
+     save_errno = errno;
+ 
+     g_free (wfilename);
+diff -u -r glib-2.46.0/glib/gstdio.c glib-2.46.0.patched/glib/gstdio.c
+--- glib-2.46.0/glib/gstdio.c	2015-02-26 13:57:09.000000000 +0100
++++ glib-2.46.0.patched/glib/gstdio.c	2016-01-27 13:31:12.708987700 +0100
+@@ -493,7 +493,10 @@
+       (!g_path_is_absolute (filename) || len > g_path_skip_root (filename) - filename))
+     wfilename[len] = '\0';
+ 
+-  retval = _wstat (wfilename, buf);
++  // MSoegtrop: _wstat32i64 is the wrong function for GLocalFileStat = struct _stati64
++  // The correct function is _wstati64, see https://msdn.microsoft.com/en-us/library/14h5k7ff.aspx
++  // Also _wstat32i64 is a VC function, not a windows SDK function, see https://msdn.microsoft.com/en-us/library/aa273365(v=vs.60).aspx
++  retval = _wstati64 (wfilename, buf);
+   save_errno = errno;
+ 
+   g_free (wfilename);
diff --git a/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch b/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch
new file mode 100644
index 000000000..73a098d12
--- /dev/null
+++ b/dev/build/windows/patches_coq/gtksourceview-2.11.2.patch
@@ -0,0 +1,213 @@
+diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c
+*** gtksourceview-2.11.2.orig/gtksourceview/gtksourceiter.c	2010-05-30 12:24:14.000000000 +0200
+--- gtksourceview-2.11.2.patched/gtksourceview/gtksourceiter.c	2015-10-27 14:58:54.422888400 +0100
+***************
+*** 80,86 ****
+  	/* If string contains prefix, check that prefix is not followed
+  	 * by a unicode mark symbol, e.g. that trailing 'a' in prefix
+  	 * is not part of two-char a-with-hat symbol in string. */
+! 	return type != G_UNICODE_COMBINING_MARK &&
+  		type != G_UNICODE_ENCLOSING_MARK &&
+  		type != G_UNICODE_NON_SPACING_MARK;
+  }
+--- 80,86 ----
+  	/* If string contains prefix, check that prefix is not followed
+  	 * by a unicode mark symbol, e.g. that trailing 'a' in prefix
+  	 * is not part of two-char a-with-hat symbol in string. */
+! 	return type != G_UNICODE_SPACING_MARK &&
+  		type != G_UNICODE_ENCLOSING_MARK &&
+  		type != G_UNICODE_NON_SPACING_MARK;
+  }
+diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c
+*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.c	2010-05-30 12:24:14.000000000 +0200
+--- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.c	2015-10-27 14:55:30.294477600 +0100
+***************
+*** 274,280 ****
+   * containg a list of language files directories.
+   * The array is owned by @lm and must not be modified.
+   */
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
+--- 274,280 ----
+   * containg a list of language files directories.
+   * The array is owned by @lm and must not be modified.
+   */
+! const gchar* const *
+  gtk_source_language_manager_get_search_path (GtkSourceLanguageManager *lm)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
+***************
+*** 392,398 ****
+   * available languages or %NULL if no language is available. The array
+   * is owned by @lm and must not be modified.
+   */
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
+--- 392,398 ----
+   * available languages or %NULL if no language is available. The array
+   * is owned by @lm and must not be modified.
+   */
+! const gchar* const *
+  gtk_source_language_manager_get_language_ids (GtkSourceLanguageManager *lm)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_LANGUAGE_MANAGER (lm), NULL);
+diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h
+*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcelanguagemanager.h	2009-11-15 00:41:33.000000000 +0100
+--- gtksourceview-2.11.2.patched/gtksourceview/gtksourcelanguagemanager.h	2015-10-27 14:55:30.518500000 +0100
+***************
+*** 62,74 ****
+  
+  GtkSourceLanguageManager *gtk_source_language_manager_get_default		(void);
+  
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  			  gtk_source_language_manager_get_search_path		(GtkSourceLanguageManager *lm);
+  
+  void			  gtk_source_language_manager_set_search_path		(GtkSourceLanguageManager *lm,
+  										 gchar                   **dirs);
+  
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  			  gtk_source_language_manager_get_language_ids		(GtkSourceLanguageManager *lm);
+  
+  GtkSourceLanguage	 *gtk_source_language_manager_get_language		(GtkSourceLanguageManager *lm,
+--- 62,74 ----
+  
+  GtkSourceLanguageManager *gtk_source_language_manager_get_default		(void);
+  
+! const gchar* const *
+  			  gtk_source_language_manager_get_search_path		(GtkSourceLanguageManager *lm);
+  
+  void			  gtk_source_language_manager_set_search_path		(GtkSourceLanguageManager *lm,
+  										 gchar                   **dirs);
+  
+! const gchar* const *
+  			  gtk_source_language_manager_get_language_ids		(GtkSourceLanguageManager *lm);
+  
+  GtkSourceLanguage	 *gtk_source_language_manager_get_language		(GtkSourceLanguageManager *lm,
+diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c
+*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.c	2010-05-30 12:24:14.000000000 +0200
+--- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.c	2015-10-27 14:55:30.545502700 +0100
+***************
+*** 310,316 ****
+   *
+   * Since: 2.0
+   */
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL);
+--- 310,316 ----
+   *
+   * Since: 2.0
+   */
+! const gchar* const *
+  gtk_source_style_scheme_get_authors (GtkSourceStyleScheme *scheme)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME (scheme), NULL);
+***************
+*** 318,324 ****
+  	if (scheme->priv->authors == NULL)
+  		return NULL;
+  
+! 	return (G_CONST_RETURN gchar* G_CONST_RETURN *)scheme->priv->authors->pdata;
+  }
+  
+  /**
+--- 318,324 ----
+  	if (scheme->priv->authors == NULL)
+  		return NULL;
+  
+! 	return (const gchar* const *)scheme->priv->authors->pdata;
+  }
+  
+  /**
+diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h
+*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestylescheme.h	2010-03-29 15:02:56.000000000 +0200
+--- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestylescheme.h	2015-10-27 14:55:30.565504700 +0100
+***************
+*** 61,67 ****
+  const gchar             *gtk_source_style_scheme_get_name       (GtkSourceStyleScheme *scheme);
+  const gchar             *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme);
+  
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  			 gtk_source_style_scheme_get_authors	(GtkSourceStyleScheme *scheme);
+  
+  const gchar             *gtk_source_style_scheme_get_filename	(GtkSourceStyleScheme *scheme);
+--- 61,67 ----
+  const gchar             *gtk_source_style_scheme_get_name       (GtkSourceStyleScheme *scheme);
+  const gchar             *gtk_source_style_scheme_get_description(GtkSourceStyleScheme *scheme);
+  
+! const gchar* const *
+  			 gtk_source_style_scheme_get_authors	(GtkSourceStyleScheme *scheme);
+  
+  const gchar             *gtk_source_style_scheme_get_filename	(GtkSourceStyleScheme *scheme);
+diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c
+*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.c	2010-05-30 12:24:14.000000000 +0200
+--- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.c	2015-10-27 14:55:30.583506500 +0100
+***************
+*** 515,521 ****
+   * of string containing the search path.
+   * The array is owned by the @manager and must not be modified.
+   */
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
+--- 515,521 ----
+   * of string containing the search path.
+   * The array is owned by the @manager and must not be modified.
+   */
+! const gchar* const *
+  gtk_source_style_scheme_manager_get_search_path (GtkSourceStyleSchemeManager *manager)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
+***************
+*** 554,560 ****
+   * of string containing the ids of the available style schemes or %NULL if no
+   * style scheme is available. The array is owned by the @manager and must not be modified.
+   */
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
+--- 554,560 ----
+   * of string containing the ids of the available style schemes or %NULL if no
+   * style scheme is available. The array is owned by the @manager and must not be modified.
+   */
+! const gchar* const *
+  gtk_source_style_scheme_manager_get_scheme_ids (GtkSourceStyleSchemeManager *manager)
+  {
+  	g_return_val_if_fail (GTK_IS_SOURCE_STYLE_SCHEME_MANAGER (manager), NULL);
+diff -c -r gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h
+*** gtksourceview-2.11.2.orig/gtksourceview/gtksourcestyleschememanager.h	2009-11-15 00:41:33.000000000 +0100
+--- gtksourceview-2.11.2.patched/gtksourceview/gtksourcestyleschememanager.h	2015-10-27 14:56:24.498897500 +0100
+***************
+*** 73,84 ****
+  void 			 gtk_source_style_scheme_manager_prepend_search_path   (GtkSourceStyleSchemeManager	*manager,
+  						    				 const gchar			*path);
+  
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  			 gtk_source_style_scheme_manager_get_search_path	(GtkSourceStyleSchemeManager	*manager);
+  
+  void			 gtk_source_style_scheme_manager_force_rescan		(GtkSourceStyleSchemeManager	*manager);
+  
+! G_CONST_RETURN gchar* G_CONST_RETURN *
+  			 gtk_source_style_scheme_manager_get_scheme_ids		(GtkSourceStyleSchemeManager	*manager);
+  
+  GtkSourceStyleScheme	*gtk_source_style_scheme_manager_get_scheme		(GtkSourceStyleSchemeManager	*manager,
+--- 73,84 ----
+  void 			 gtk_source_style_scheme_manager_prepend_search_path   (GtkSourceStyleSchemeManager	*manager,
+  						    				 const gchar			*path);
+  
+! const gchar* const *
+  			 gtk_source_style_scheme_manager_get_search_path	(GtkSourceStyleSchemeManager	*manager);
+  
+  void			 gtk_source_style_scheme_manager_force_rescan		(GtkSourceStyleSchemeManager	*manager);
+  
+! const gchar* const *
+  			 gtk_source_style_scheme_manager_get_scheme_ids		(GtkSourceStyleSchemeManager	*manager);
+  
+  GtkSourceStyleScheme	*gtk_source_style_scheme_manager_get_scheme		(GtkSourceStyleSchemeManager	*manager,
diff --git a/dev/build/windows/patches_coq/isl-0.14.patch b/dev/build/windows/patches_coq/isl-0.14.patch
new file mode 100644
index 000000000..f3b8ead1a
--- /dev/null
+++ b/dev/build/windows/patches_coq/isl-0.14.patch
@@ -0,0 +1,11 @@
+--- orig.isl-0.14/configure	2014-10-26 08:36:32.000000000 +0100
++++ isl-0.14/configure	2016-10-10 18:16:01.430224500 +0200
+@@ -8134,7 +8134,7 @@
+      lt_sysroot=`$CC --print-sysroot 2>/dev/null`
+    fi
+    ;; #(
+- /*)
++ /*|[A-Z]:\\*|[A-Z]:/*)
+    lt_sysroot=`echo "$with_sysroot" | sed -e "$sed_quote_subst"`
+    ;; #(
+  no|'')
diff --git a/dev/build/windows/patches_coq/lablgtk-2.18.3.patch b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
new file mode 100644
index 000000000..0691c1fc8
--- /dev/null
+++ b/dev/build/windows/patches_coq/lablgtk-2.18.3.patch
@@ -0,0 +1,87 @@
+diff -u -r lablgtk-2.18.3/configure lablgtk-2.18.3.patched/configure
+--- lablgtk-2.18.3/configure	2014-10-29 08:51:05.000000000 +0100
++++ lablgtk-2.18.3.patched/configure	2015-10-29 08:58:08.543985500 +0100
+@@ -2667,7 +2667,7 @@
+ fi
+ 
+ 
+-if test "`$OCAMLFIND printconf stdlib`" != "`$CAMLC -where`"; then
++if test "`$OCAMLFIND printconf stdlib | tr '\\' '/'`" != "`$CAMLC -where | tr '\\' '/'`"; then
+   { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Ignoring ocamlfind" >&5
+ $as_echo "$as_me: WARNING: Ignoring ocamlfind" >&2;}
+   OCAMLFIND=no
+
+diff -u -r lablgtk-2.18.3/src/glib.mli lablgtk-2.18.3.patched/src/glib.mli
+--- lablgtk-2.18.3/src/glib.mli	2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3.patched/src/glib.mli	2016-01-25 09:50:59.884715200 +0100
+@@ -75,6 +75,7 @@
+   type condition = [ `ERR | `HUP | `IN | `NVAL | `OUT | `PRI]
+   type id
+   val channel_of_descr : Unix.file_descr -> channel
++  val channel_of_descr_socket : Unix.file_descr -> channel
+   val add_watch :
+     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+   val remove : id -> unit
+
+diff -u -r lablgtk-2.18.3/src/glib.ml lablgtk-2.18.3.patched/src/glib.ml
+--- lablgtk-2.18.3/src/glib.ml	2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3.patched/src/glib.ml	2016-01-25 09:50:59.891715900 +0100
+@@ -72,6 +72,8 @@
+   type id
+   external channel_of_descr : Unix.file_descr -> channel
+     = "ml_g_io_channel_unix_new"
++  external channel_of_descr_socket : Unix.file_descr -> channel
++    = "ml_g_io_channel_unix_new_socket"
+   external remove : id -> unit = "ml_g_source_remove"
+   external add_watch :
+     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
+
+diff -u -r lablgtk-2.18.3/src/ml_glib.c lablgtk-2.18.3.patched/src/ml_glib.c
+--- lablgtk-2.18.3/src/ml_glib.c	2014-10-29 08:51:06.000000000 +0100
++++ lablgtk-2.18.3.patched/src/ml_glib.c	2016-01-25 09:50:59.898716600 +0100
+@@ -25,6 +25,8 @@
+ #include <string.h>
+ #include <locale.h>
+ #ifdef _WIN32
++/* to kill a #warning: include winsock2.h before windows.h */
++#include <winsock2.h>
+ #include "win32.h"
+ #include <wtypes.h>
+ #include <io.h>
+@@ -38,6 +40,11 @@
+ #include <caml/callback.h>
+ #include <caml/threads.h>
+ 
++#ifdef _WIN32
++/* for Socket_val */
++#include <caml/unixsupport.h>
++#endif
++
+ #include "wrappers.h"
+ #include "ml_glib.h"
+ #include "glib_tags.h"
+@@ -325,14 +332,23 @@
+ 
+ #ifndef _WIN32
+ ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
++CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) {
++  return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1))); 
++}
+ 
+ #else
+ CAMLprim value ml_g_io_channel_unix_new(value wh)
+ {
+   return Val_GIOChannel_noref
+-    (g_io_channel_unix_new
++    (g_io_channel_win32_new_fd
+      (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY)));
+ }
++
++CAMLprim value ml_g_io_channel_unix_new_socket(value wh)
++{
++  return Val_GIOChannel_noref
++    (g_io_channel_win32_new_socket(Socket_val(wh)));
++}
+ #endif
+ 
+ static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c,
diff --git a/dev/build/windows/patches_coq/ln.c b/dev/build/windows/patches_coq/ln.c
new file mode 100644
index 000000000..5e02c72bb
--- /dev/null
+++ b/dev/build/windows/patches_coq/ln.c
@@ -0,0 +1,137 @@
+// (C) 2016 Intel Deutschland GmbH
+// Author: Michael Soegtrop
+// Released to the public under CC0
+// See https://creativecommons.org/publicdomain/zero/1.0/
+
+// Windows drop in repacement for Linux ln
+// Supports command form "ln TARGET LINK_NAME"
+// Supports -s and -f options
+// Does not support hard links to folders (but symlinks are ok)
+
+#include <windows.h>
+#include <stdio.h>
+#include <tchar.h>
+
+// Cygwin MinGW doesn't have this Vista++ function in windows.h
+#ifdef UNICODE
+    WINBASEAPI BOOLEAN APIENTRY CreateSymbolicLinkW ( LPCWSTR, LPCWSTR, DWORD );
+    #define CreateSymbolicLink  CreateSymbolicLinkW
+    #define CommandLineToArgv CommandLineToArgvW
+#else
+    WINBASEAPI BOOLEAN APIENTRY CreateSymbolicLinkA ( LPCSTR, LPCSTR, DWORD );
+    #define CreateSymbolicLink  CreateSymbolicLinkA
+    #define CommandLineToArgv CommandLineToArgvA
+#endif
+#define SYMBOLIC_LINK_FLAG_DIRECTORY 1
+
+int WINAPI WinMain( HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLineA, int nShowCmd )
+{
+    int iarg;
+    BOOL symbolic = FALSE;
+    BOOL force = FALSE;
+    BOOL folder;
+    const _TCHAR *target;
+    const _TCHAR *link;
+    LPTSTR lpCmdLine; 
+    int argc;
+    LPTSTR *argv;
+
+    // Parse command line
+    // This is done explicitly here for two reasons
+    // 1.) MinGW doesn't seem to support _tmain, wWinMain and the like
+    // 2.) We want to make sure that CommandLineToArgv is used
+    lpCmdLine = GetCommandLine();
+    argv = CommandLineToArgv( lpCmdLine, &argc );
+    
+    // Get target and link name
+    if( argc<3 )
+    {
+        _ftprintf( stderr, _T("Expecting at least 2 arguments, got %d\n"), argc-1 );
+        return 1;
+    }
+    target = argv[argc-2];
+    link = argv[argc-1];
+
+    // Parse options
+    // The last two arguments are interpreted as file names
+    // All other arguments must be -s or -f os multi letter options like -sf
+    for(iarg=1; iarg<argc-2; iarg++ )
+    {
+        const _TCHAR *pos = argv[iarg]; 
+        if( *pos != _T('-') )
+        {
+            _ftprintf( stderr, _T("Command line option expected in argument %d\n"), iarg );
+            return 1;
+        }
+        pos ++;
+
+        while( *pos )
+        {
+            switch( *pos )
+            {
+                case _T('s') : symbolic = TRUE; break;
+                case _T('f') : force = TRUE; break;
+                default : 
+                    _ftprintf( stderr, _T("Unknown option '%c'\n"), *pos );
+                    return 1;
+            }
+            pos ++;
+        }
+    }
+    
+    #ifdef IGNORE_SYMBOLIC
+        symbolic = FALSE;
+    #endif
+    
+    // Check if link already exists - delete it if force is given or abort
+    {
+        if( GetFileAttributes(link) != INVALID_FILE_ATTRIBUTES )
+        {
+            if( force )
+            {
+                if( !DeleteFile( link ) )
+                {
+                    _ftprintf( stderr, _T("Error deleting file '%s'\n"), link );
+                    return 1;
+                }
+            }
+            else
+            {
+                _ftprintf( stderr, _T("File '%s' exists!\n"), link );
+                return 1;
+            }
+        }
+    }
+    
+    // Check if target is a folder
+    folder = ( (GetFileAttributes(target) & FILE_ATTRIBUTE_DIRECTORY) ) != 0;
+    
+    // Create link
+    if(symbolic)
+    {
+        if( !CreateSymbolicLink( link, target, folder ? SYMBOLIC_LINK_FLAG_DIRECTORY : 0 ) )
+        {
+            _ftprintf( stderr, _T("Error creating symbolic link '%s' -> '%s'!\n"), link, target );
+            return 1;
+        }
+    }
+    else
+    {
+        if( folder )
+        {
+            _ftprintf( stderr, _T("Cannot create hard link to folder") );
+            return 1;
+        }
+        else
+        {
+            if( !CreateHardLink( link, target, NULL ) )
+            {
+                _ftprintf( stderr, _T("Error creating hard link '%s' -> '%s'!\n"), link, target );
+                return 1;
+            }
+        }
+    }
+    
+    // Everything is fine
+    return 0;
+}
\ No newline at end of file
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 800194b1d..5fe88bf33 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -66,6 +66,8 @@ kernel/closure.ml{,i} -> kernel/cClosure.ml{,i}
 lib/errors.ml{,i} -> lib/cErrors.ml{,i}
 toplevel/cerror.ml{,i} -> toplevel/explainErr.mli{,i}
 
+All IDE-specific files, including the XML protocol have been moved to ide/
+
 ** Reduction functions **
 
 In closure.ml, we introduced the more precise reduction flags fMATCH, fFIX,
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh
deleted file mode 100755
index 51d428dd1..000000000
--- a/dev/make-installer-win32.sh
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/sh
-
-set -e
-
-NSIS="$BASE/NSIS/makensis"
-ZIP=_make.zip
-URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download
-URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download
-
-[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no
-make -j2 
-if [ ! -e bin/make.exe ]; then
-  wget -O $ZIP $URL1 && 7z x $ZIP "bin/*"
-  wget -O $ZIP $URL2 && 7z x $ZIP "bin/*"
-  rm -rf $ZIP
-fi
-VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
-cd dev/nsis
-"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win32" coq.nsi
-echo Installer:
-ls -h $PWD/*exe
-cd ../..
diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh
deleted file mode 100755
index 438f4ae5b..000000000
--- a/dev/make-installer-win64.sh
+++ /dev/null
@@ -1,28 +0,0 @@
-#!/bin/sh
-
-set -e
-
-NSIS="$BASE/NSIS/makensis"
-ZIP=_make.zip
-URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download
-URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download
-
-[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no
-make -j2 coqide
-mkdir -p bin32
-cp bin/* bin32/
-make clean
-make archclean
-( . ${BASE}_64/environ && ./configure -debug -prefix ./ -with-doc no && make -j2 && make ide/coqidetop.cmxs )
-cp bin32/coqide* bin/
-if [ ! -e bin/make.exe ]; then
-  wget -O $ZIP $URL1 && 7z x $ZIP "bin/*"
-  wget -O $ZIP $URL2 && 7z x $ZIP "bin/*"
-  rm -rf $ZIP
-fi
-VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
-cd dev/nsis
-"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win64" coq.nsi
-echo Installer:
-ls -h $PWD/*exe
-cd ../..
diff --git a/dev/make-sdk-win32.sh b/dev/make-sdk-win32.sh
deleted file mode 100755
index 0112324d4..000000000
--- a/dev/make-sdk-win32.sh
+++ /dev/null
@@ -1,370 +0,0 @@
-#!/bin/bash
-
-# To run this script install cygwin by running setup-x86.exe from cygwin.com
-# Install the standard packages plus wget.  Then run this script.
-
-# Sworn by Enrico Tassi <enrico.tassi@inra.fr>
-# Modified to support other directories and almost support spaces in paths
-# by Jason Gross <jgross@mit.edu>
-# License: Expat/MIT http://opensource.org/licenses/MIT
-
-# This script reads the following environment variables:
-# VERBOSE     - set to non-empty to have wget/this script be more verbose, for debugging purposes
-# BASE        - set to non-empty to give a different location for the zip file, e.g., if /cygdrive/c is full or doesn't exist
-
-set -e
-if [ ! -z "$VERBOSE" ]
-then
-  set -x
-fi
-
-# Resources
-ocaml=ocaml-4.01.0-i686-mingw64-installer3.exe
-glib=base-windows-0.18.1.1.13.356@BUILD_ec06e9.txz
-gtk=base-gtk-2.24.18.1.58@BUILD_594ca8.txz
-lablgtk=lablgtk-2.18.0.tar.gz
-camlp5=camlp5-6.11.tgz
-nsis=nsis-2.46-setup.exe
-
-ocaml_URL='http://yquem.inria.fr/~protzenk/caml-installer/'$ocaml
-lablgtk_URL='https://forge.ocamlcore.org/frs/download.php/1261/'$lablgtk
-glib_URL='http://dl.arirux.de/5/binaries32/'$glib
-gtk_URL='http://dl.arirux.de/5/binaries32/'$gtk
-camlp5_URL='http://pauillac.inria.fr/~ddr/camlp5/distrib/src/'$camlp5
-nsis_URL='http://netcologne.dl.sourceforge.net/project/nsis/NSIS%202/2.46/'$nsis
-
-cygwin=setup-${HOSTTYPE/i6/x}.exe
-cygwin_URL='http://cygwin.com/'$cygwin
-cygwin_PKGS=p7zip,zip,sed,make,mingw64-i686-gcc-g++,mingw64-i686-gcc-core,mingw64-i686-gcc,patch,rlwrap,libreadline6,diffutils
-
-has_spaces() {
-    test -z "$2"
-}
-# utilities
-# http://www.dependencywalker.com/depends22_x86.zip
-
-# The SDK itself
-REVISION=85-1
-# support for working on computers that don't have a C: drive
-if [ -z "$BASE" ]
-then
-  TRUE_BASE=/cygdrive/c
-else
-  # get absolute path
-  TRUE_BASE="$(readlink -f "$BASE")"
-fi
-BASE="$TRUE_BASE/CoqSDK-$REVISION"
-
-if [ -z "$VERBOSE" ]
-then
-  WGET_ARGS="-N -q"
-else
-  WGET_ARGS="-N"
-fi
-
-# Windows has a version of FIND in C:/Windows/system32/find, and we don't want to use that
-if [ -x /usr/bin/find ]
-then
-  FIND=/usr/bin/find
-else
-  echo "WARNING: /usr/bin/find does not exist.  Falling back on:"
-  which find
-  FIND=find
-fi
-
-WGET_ARGS="-N -q"
-
-if [ "$(has_spaces $BASE; echo $?)" -ne 0 ]; then
-  echo "ERROR: The current base directory ($BASE) has spaces."
-  echo "ERROR: building lablgtk would fail."
-  exit 1
-fi
-
-cyg_install() {
-  if [ ! -e "$cygwin" ]; then wget $WGET_ARGS "$cygwin_URL"; fi
-  chmod a+x "$cygwin"
-  cygstart -w "$cygwin" -q -P $@
-}
-
-sanity_check() {
-  echo "Check: wget."
-  (which wget) || \
-	  (echo "Please install wget using the cygwin installer and retry.";\
-	   exit 1)
-  echo "Check: 7z, gcc.  If it fails wait for cygwin to complete and retry"
-  (which 7z && which i686-w64-mingw32-gcc) || \
-	  (echo "Some cygwin package is not installed.";\
-	   echo "Please wait for cygwin to finish and retry.";\
-	   cyg_install $cygwin_PKGS;\
-	   exit 1)
-}
-
-install_base() {
-  echo "Setting up $BASE"
-  rm -rf "$BASE"
-  mkdir -p "$BASE"
-}
-
-make_environ() {
-  echo "Setting up $BASE/environ"
-  pushd "$BASE" >/dev/null
-  cat > environ <<- EOF
-	cyg_install() {
-	  if [ ! -e "$cygwin" ]; then wget $WGET_ARGS "$cygwin_URL"; fi
-	  chmod a+x "$cygwin"
-	  cygstart -w "$cygwin" -q -P \$@
-	}
-	# Sanity checks: is the mingw64-i686-gcc package installed?
-	(which i686-w64-mingw32-gcc && which make && which sed) || \\
-		(echo "Some cygwin package is not installed.";\\
-	         echo "Please wait for cygwin to finish and retry.";\\
-	 	 cyg_install $cygwin_PKGS;\\
-		 exit 1) || exit 1
-
-	export BASE="\$( cd "\$( dirname "\${BASH_SOURCE[0]}" )" && pwd )"
-	export PATH="\$BASE/bin:\$PATH"
-	export OCAMLLIB="\$(cygpath -m "\$BASE")/lib"
-	export OCAMLFIND_CONF="\$(cygpath -m "\$BASE")/etc/findlib.conf"
-	sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/lib/ld.conf.in" \\
-	        > "\$BASE/lib/ld.conf"
-	sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/lib/topfind.in" \\
-	        > "\$BASE/lib/topfind"
-	sed s"|@BASE@|\$(cygpath -m "\$BASE")|g" "\$BASE/etc/findlib.conf.in" \\
-	        > "\$BASE/etc/findlib.conf"
-	echo "Good.  You can now build Coq and Coqide from cygwin."
-	EOF
-  popd >/dev/null
-}
-
-download() {
-  echo "Downloading some software:"
-  if [ ! -e "$ocaml" ]; then
-    echo "- downloading OCaml..."
-    wget $WGET_ARGS "$ocaml_URL"
-  fi
-  chmod a+x "$ocaml"
-  if [ ! -e "$lablgtk" ]; then
-    echo "- downloading lablgtk..."
-    wget $WGET_ARGS --no-check-certificate "$lablgtk_URL"
-  fi
-  if [ ! -e "$gtk" ]; then
-    echo "- downloading gtk..."
-    wget $WGET_ARGS "$gtk_URL"
-  fi
-  if [ ! -e "$glib" ]; then
-    echo "- downloading glib..."
-    wget $WGET_ARGS "$glib_URL"
-  fi
-  if [ ! -e "$camlp5" ]; then
-    echo "- downloading camlp5..."
-    wget $WGET_ARGS "$camlp5_URL"
-  fi
-  if [ ! -e "$nsis" ]; then
-    echo "- downloading nsis..."
-    wget $WGET_ARGS "$nsis_URL"
-  fi
-}
-
-cleanup() {
-  rm -rf tmp build
-}
-
-install_gtk() {
-  echo "Installing $glib"
-  tar -xJf "$glib" -C "$BASE"
-  echo "Installing $gtk"
-  tar -xJf "$gtk" -C "$BASE"
-}
-
-install_ocaml() {
-  echo "Installing $ocaml"
-  mkdir -p tmp
-  7z -otmp x "$ocaml" >/dev/null
-  cp -r tmp/\$_OUTDIR/bin "$BASE/"
-  cp -r tmp/bin "$BASE/"
-  cp -r tmp/\$_OUTDIR/lib "$BASE/"
-  cp -r tmp/lib "$BASE/"
-  cp -r tmp/\$_OUTDIR/etc "$BASE/"
-  "$FIND" "$BASE" -name '*.dll' -o -name '*.exe' | tr '\n' '\0' \
-	  | xargs -0 chmod a+x
-  mv "$BASE/lib/topfind" "$BASE/lib/topfind.in"
-  sed -i 's|@SITELIB@|@BASE@/lib/site-lib|g' "$BASE/lib/topfind.in"
-  cat > "$BASE/lib/ld.conf.in" <<- EOF
-	@BASE@/lib
-	@BASE@/lib/stublibs
-	EOF
-  cat > "$BASE/etc/findlib.conf.in" <<- EOF
-	destdir="@BASE@/lib/site-lib"
-	path="@BASE@/lib/site-lib"
-	stdlib="@BASE@/lib"
-	ldconf="@BASE@/lib/ld.conf"
-	ocamlc="ocamlc.opt"
-	ocamlopt="ocamlopt.opt"
-	ocamldep="ocamldep.opt"
-	ocamldoc="ocamldoc.opt"
-	EOF
-  cp "$BASE/lib/topdirs.cmi" "$BASE/lib/compiler-libs/"
-}
-
-build_install_lablgtk() {
-  echo "Building $lablgtk"
-  mkdir -p build
-  tar -xzf "$lablgtk" -C build
-  cd build/lablgtk-*
-  patch -p1 <<EOT
---- lablgtk-2.18.0/src/glib.mli	2013-10-01 01:31:50.000000000 -0700
-+++ lablgtk-2.18.0.new/src/glib.mli	2013-12-06 11:57:34.203675200 -0800
-@@ -75,6 +75,7 @@
-   type condition = [ \`ERR | \`HUP | \`IN | \`NVAL | \`OUT | \`PRI]
-   type id
-   val channel_of_descr : Unix.file_descr -> channel
-+  val channel_of_descr_socket : Unix.file_descr -> channel
-   val add_watch :
-     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
-   val remove : id -> unit
---- lablgtk-2.18.0/src/glib.ml	2013-10-01 01:31:50.000000000 -0700
-+++ lablgtk-2.18.0.new/src/glib.ml	2013-12-06 11:57:53.070804800 -0800
-@@ -72,6 +72,8 @@
-   type id
-   external channel_of_descr : Unix.file_descr -> channel
-     = "ml_g_io_channel_unix_new"
-+  external channel_of_descr_socket : Unix.file_descr -> channel
-+    = "ml_g_io_channel_unix_new_socket"
-   external remove : id -> unit = "ml_g_source_remove"
-   external add_watch :
-     cond:condition list -> callback:(condition list -> bool) -> ?prio:int -> channel -> id
---- lablgtk-2.18.0/src/ml_glib.c	2013-10-01 01:31:50.000000000 -0700
-+++ lablgtk-2.18.0.new/src/ml_glib.c	2013-12-10 02:03:33.940371800 -0800
-@@ -25,6 +25,8 @@
- #include <string.h>
- #include <locale.h>
- #ifdef _WIN32
-+/* to kill a #warning: include winsock2.h before windows.h */
-+#include <winsock2.h>
- #include "win32.h"
- #include <wtypes.h>
- #include <io.h>
-@@ -38,6 +40,11 @@
- #include <caml/callback.h>
- #include <caml/threads.h>
-
-+#ifdef _WIN32
-+/* for Socket_val */
-+#include <caml/unixsupport.h>
-+#endif
-+
- #include "wrappers.h"
- #include "ml_glib.h"
- #include "glib_tags.h"
-@@ -325,14 +332,23 @@
-
- #ifndef _WIN32
- ML_1 (g_io_channel_unix_new, Int_val, Val_GIOChannel_noref)
-+CAMLprim value ml_g_io_channel_unix_new_socket (value arg1) {
-+  return Val_GIOChannel_noref (g_io_channel_unix_new (Int_val (arg1)));
-+}
-
- #else
- CAMLprim value ml_g_io_channel_unix_new(value wh)
- {
-   return Val_GIOChannel_noref
--    (g_io_channel_unix_new
-+    (g_io_channel_win32_new_fd
-      (_open_osfhandle((long)*(HANDLE*)Data_custom_val(wh), O_BINARY)));
- }
-+
-+CAMLprim value ml_g_io_channel_unix_new_socket(value wh)
-+{
-+  return Val_GIOChannel_noref
-+    (g_io_channel_win32_new_socket(Socket_val(wh)));
-+}
- #endif
-
- static gboolean ml_g_io_channel_watch(GIOChannel *s, GIOCondition c,
-EOT
-  #sed -i s'/$PKG_CONFIG/"$PKG_CONFIG"/g' configure
-  #sed -i s'/""$PKG_CONFIG""/"$PKG_CONFIG"/g' configure
-  ./configure --disable-gtktest --prefix="$(cygpath -m "$BASE")" \
-	  >log-configure 2>&1
-  sed -i 's?\\?/?g' config.make
-  make >log-make 2>&1
-  make opt >>log-make 2>&1
-  #echo "Testing $lablgtk"
-  #cd src
-  #./lablgtk2 ../examples/calc.ml
-  #./lablgtk2 -all ../examples/calc.ml
-  #cd ..
-  echo "Installing $lablgtk"
-  make install >>log-make 2>&1
-  cd ../..
-}
-
-build_install_camlp5() {
-  echo "Building $camlp5"
-  mkdir -p build
-  tar -xzf "$camlp5" -C build
-  cd build/camlp5-*
-  ./configure >log-configure 2>&1
-  sed -i 's/EXT_OBJ=.obj/EXT_OBJ=.o/' config/Makefile
-  sed -i 's/EXT_LIB=.lib/EXT_LIB=.a/' config/Makefile
-  make world.opt >log-make 2>&1
-  echo "Installing $camlp5"
-  make install >>log-make 2>&1
-  cd ../..
-}
-
-install_nsis() {
-  echo "Installing $nsis"
-  rm -rf tmp
-  mkdir -p tmp
-  7z -otmp x $nsis >/dev/null
-  mkdir "$BASE/NSIS"
-  cp -r tmp/\$_OUTDIR/* "$BASE/NSIS"
-  rm -rf tmp/\$_OUTDIR
-  rm -rf tmp/\$PLUGINSDIR
-  cp -r tmp/* "$BASE/NSIS"
-}
-
-zip_sdk() {
-  echo "Generating CoqSDK-${REVISION}.zip"
-  here="`pwd`"
-  cd "$BASE/.."
-  rm -f "$here/CoqSDK-${REVISION}.zip"
-  zip -q -r "$here/CoqSDK-${REVISION}.zip" "$(basename "$BASE")"
-  cd "$here"
-}
-
-diet_sdk() {
-  rm -rf "$BASE"/+*
-  rm -rf "$BASE"/bin/camlp4*
-  rm -rf "$BASE"/lib/camlp4/
-  rm -rf "$BASE"/lib/site-lib/camlp4/
-}
-
-victory(){
-  echo "Output file: CoqSDK-${REVISION}.zip "\
-	  "(`du -sh CoqSDK-${REVISION}.zip | cut -f 1`)"
-  echo "Usage: unpack and source the environ file at its root"
-}
-
-if [ -z "$1" ]; then
-  sanity_check
-  download
-  cleanup
-  install_base
-  install_nsis
-  install_ocaml
-  install_gtk
-  make_environ
-  . "$BASE/environ"
-  build_install_lablgtk
-  build_install_camlp5
-  diet_sdk
-  make_environ
-  zip_sdk
-  cleanup
-  victory
-else
-  # just one step
-  $1
-fi