Merge branch 'v8.6'

73 files changed, 3606 insertions, 486 deletions

diff --git a/Makefile.ci b/Makefile.ci
index 3be90c0a3..c8bc09fdc 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -24,4 +24,4 @@ CI_TARGETS=ci-all \
 
 # Generic rule, we use make to easy travis integraton with mixed rules
 $(CI_TARGETS): ci-%:
-	./dev/ci/ci-$*.sh
+	+./dev/ci/ci-$*.sh
diff --git a/configure b/configure
index 09585e59e..4f11b2c2d 100755
--- a/configure
+++ b/configure
@@ -3,7 +3,7 @@
 ## This micro-configure shell script is here only to
 ## launch the real configuration via ocaml
 
-cmd=ocaml
+ocaml=ocaml
 script=./configure.ml
 
 if [ ! -f $script ]; then
@@ -16,17 +16,18 @@ fi
 ## Parse the args, only looking for -camldir
 ## We avoid using shift to keep "$@" intact
 
+cmd=$ocaml
 last=
 for i; do
    case $last in
-       -camldir|--camldir) cmd="$i/ocaml"; break;;
+       -camldir) cmd="$i/$ocaml"; break;;
    esac
    last=$i
 done
 
 ## We check that $cmd is ok before the real exec $cmd
 
-`$cmd -version > /dev/null 2>&1` && exec $cmd $script "$@"
+`$cmd -version > /dev/null 2>&1` && exec $cmd -w "-3" $script "$@"
 
 ## If we're still here, something is wrong with $cmd
 
diff --git a/configure.ml b/configure.ml
index 549b32772..c75c3d7e1 100644
--- a/configure.ml
+++ b/configure.ml
@@ -364,6 +364,8 @@ let args_options = Arg.align [
     " Force OCaml version";
   "-warn-error", Arg.Set Prefs.warn_error,
     " Make OCaml warnings into errors";
+  "-camldir", Arg.String (fun _ -> ()),
+    "<dir> Specifies path to 'ocaml' for running configure script";
 ]
 
 let parse_args () =
diff --git a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
index bdcb01db9..9dbce1920 100644
--- a/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
+++ b/dev/build/windows/MakeCoq_84pl6_abs_ocaml.bat
@@ -1,3 +1,16 @@
+@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 ========== BUILD COQ ==========

+

 call MakeCoq_SetRootPath

 

 call MakeCoq_MinGW.bat ^

@@ -6,5 +19,10 @@ call MakeCoq_MinGW.bat ^
   -ocaml=Y ^

   -make=Y ^

   -coqver=8.4pl6 ^

-  -destcyg=%ROOTPATH%\cygwin_coq64_84pl6_abs ^

-  -destcoq=%ROOTPATH%\coq64_84pl6_abs

+  -destcyg="%ROOTPATH%\cygwin_coq64_84pl6_abs" ^

+  -destcoq="%ROOTPATH%\coq64_84pl6_abs"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_84pl6_abs_ocaml.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
index 2e4a692e9..7faf3e9ce 100644
--- a/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
+++ b/dev/build/windows/MakeCoq_85pl2_abs_ocaml.bat
@@ -1,3 +1,16 @@
+@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 ========== BUILD COQ ==========

+

 call MakeCoq_SetRootPath

 

 call MakeCoq_MinGW.bat ^

@@ -6,5 +19,10 @@ call MakeCoq_MinGW.bat ^
   -ocaml=Y ^

   -make=Y ^

   -coqver=8.5pl2 ^

-  -destcyg=%ROOTPATH%\cygwin_coq64_85pl2_abs ^

-  -destcoq=%ROOTPATH%\coq64_85pl2_abs

+  -destcyg="%ROOTPATH%\cygwin_coq64_85pl2_abs" ^

+  -destcoq="%ROOTPATH%\coq64_85pl2_abs"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_85pl2_abs_ocaml.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
index 6e4e440a2..b719b14c5 100644
--- a/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
+++ b/dev/build/windows/MakeCoq_85pl3_abs_ocaml.bat
@@ -1,3 +1,16 @@
+@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 ========== BUILD COQ ==========

+

 call MakeCoq_SetRootPath

 

 call MakeCoq_MinGW.bat ^

@@ -6,5 +19,10 @@ call MakeCoq_MinGW.bat ^
   -ocaml=Y ^

   -make=Y ^

   -coqver=8.5pl3 ^

-  -destcyg=%ROOTPATH%\cygwin_coq64_85pl3_abs ^

-  -destcoq=%ROOTPATH%\coq64_85pl3_abs

+  -destcyg="%ROOTPATH%\cygwin_coq64_85pl3_abs" ^

+  -destcoq="%ROOTPATH%\coq64_85pl3_abs"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_85pl3_abs_ocaml.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_85pl3_installer.bat b/dev/build/windows/MakeCoq_85pl3_installer.bat
index c305e2f52..a9f4e2da2 100644
--- a/dev/build/windows/MakeCoq_85pl3_installer.bat
+++ b/dev/build/windows/MakeCoq_85pl3_installer.bat
@@ -1,8 +1,26 @@
+@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 ========== BUILD COQ ==========

+

 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

+  -destcyg="%ROOTPATH%\cygwin_coq64_85pl3_inst" ^

+  -destcoq="%ROOTPATH%\coq64_85pl3_inst"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_85pl3_installer.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_85pl3_installer_32.bat b/dev/build/windows/MakeCoq_85pl3_installer_32.bat
index d87ff5919..ef593cc63 100644
--- a/dev/build/windows/MakeCoq_85pl3_installer_32.bat
+++ b/dev/build/windows/MakeCoq_85pl3_installer_32.bat
@@ -1,8 +1,26 @@
+@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 ========== BUILD COQ ==========

+

 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

+  -destcyg="%ROOTPATH%\cygwin_coq32_85pl3_inst" ^

+  -destcoq="%ROOTPATH%\coq32_85pl3_inst"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_85pl3_installer_32.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
index f1d855a02..99a1f156b 100644
--- a/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
+++ b/dev/build/windows/MakeCoq_86git_abs_ocaml.bat
@@ -1,3 +1,16 @@
+@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 ========== BUILD COQ ==========

+

 call MakeCoq_SetRootPath

 

 call MakeCoq_MinGW.bat ^

@@ -6,5 +19,10 @@ call MakeCoq_MinGW.bat ^
   -ocaml=Y ^

   -make=Y ^

   -coqver=git-v8.6 ^

-  -destcyg=%ROOTPATH%\cygwin_coq64_86git_abs ^

-  -destcoq=%ROOTPATH%\coq64_86git_abs

+  -destcyg="%ROOTPATH%\cygwin_coq64_86git_abs" ^

+  -destcoq="%ROOTPATH%\coq64_86git_abs"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_86git_abs_ocaml.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
index 70ab42bc3..896d1cd63 100644
--- a/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
+++ b/dev/build/windows/MakeCoq_86git_abs_ocaml_gtksrc.bat
@@ -1,3 +1,16 @@
+@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 ========== BUILD COQ ==========

+

 call MakeCoq_SetRootPath

 

 call MakeCoq_MinGW.bat ^

@@ -7,5 +20,10 @@ call MakeCoq_MinGW.bat ^
   -make=Y ^

   -gtksrc=Y ^

   -coqver=git-v8.6 ^

-  -destcyg=%ROOTPATH%\cygwin_coq64_86git_abs_gtksrc ^

-  -destcoq=%ROOTPATH%\coq64_86git_abs_gtksrc

+  -destcyg="%ROOTPATH%\cygwin_coq64_86git_abs_gtksrc" ^

+  -destcoq="%ROOTPATH%\coq64_86git_abs_gtksrc"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_86git_abs_ocaml_gtksrc.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_86git_installer.bat b/dev/build/windows/MakeCoq_86git_installer.bat
index 40506318e..c4823103f 100644
--- a/dev/build/windows/MakeCoq_86git_installer.bat
+++ b/dev/build/windows/MakeCoq_86git_installer.bat
@@ -1,8 +1,26 @@
+@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 ========== BUILD COQ ==========

+

 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

+  -destcyg="%ROOTPATH%\cygwin_coq64_86git_inst" ^

+  -destcoq="%ROOTPATH%\coq64_86git_inst"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_86git_installer.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_86git_installer_32.bat b/dev/build/windows/MakeCoq_86git_installer_32.bat
index b9127c945..19146c96c 100644
--- a/dev/build/windows/MakeCoq_86git_installer_32.bat
+++ b/dev/build/windows/MakeCoq_86git_installer_32.bat
@@ -1,8 +1,26 @@
+@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 ========== BUILD COQ ==========

+

 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

+  -destcyg="%ROOTPATH%\cygwin_coq32_86git_inst" ^

+  -destcoq="%ROOTPATH%\coq32_86git_inst"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_86git_installer_32.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat b/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat
new file mode 100755
index 000000000..cf6cafaa0
--- /dev/null
+++ b/dev/build/windows/MakeCoq_86git_installer_cyglocal.bat
@@ -0,0 +1,27 @@
+@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 ========== BUILD COQ ==========

+

+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -installer=Y ^

+  -coqver=git-v8.6 ^

+  -cyglocal=Y ^

+  -destcyg="%ROOTPATH%\cygwin_coq64_86git_inst_cyglocal" ^

+  -destcoq="%ROOTPATH%\coq64_86git_inst_cyglocal"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_86git_installer_cyglocal.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 1e08cc5a3..b2efe2ddd 100644
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -18,7 +18,7 @@ REM ========== DEFAULT VALUES FOR PARAMETERS ==========
 
 REM For a description of all parameters, see ReadMe.txt
 
-SET BATCHFILE=%0
+SET BATCHFILE=%~0
 SET BATCHDIR=%~dp0
 
 REM see -arch in ReadMe.txt, but values are x86_64 or i686 (not 64 or 32)
@@ -47,9 +47,11 @@ SET SETUP=setup-x86_64.exe
 
 REM see -proxy in ReadMe.txt
 IF DEFINED HTTP_PROXY (
-  SET PROXY="%HTTP_PROXY:http://=%"
+  SET PROXY=%HTTP_PROXY:http://=%
 ) else (
-  SET PROXY=""
+  REM One can't set a variable to empty in DOS, but you can set it to a space this way.
+  REM The quotes are just there to make the space visible and to protect from "remove trailing spaces".
+  SET "PROXY= "
 )
 
 REM see -cygrepo in ReadMe.txt
@@ -82,12 +84,12 @@ SHIFT
 
 :Parse
 
-IF "%0" == "-arch" (
-  IF "%1" == "32" (
+IF "%~0" == "-arch" (
+  IF "%~1" == "32" (
     SET ARCH=i686
     SET SETUP=setup-x86.exe
   ) ELSE (
-    IF "%1" == "64" (
+    IF "%~1" == "64" (
       SET ARCH=x86_64
       SET SETUP=setup-x86_64.exe
     ) ELSE (
@@ -100,15 +102,15 @@ IF "%0" == "-arch" (
   GOTO Parse
 )
 
-IF "%0" == "-mode" (
-  IF "%1" == "mingwincygwin" (
-    SET INSTALLMODE=%1
+IF "%~0" == "-mode" (
+  IF "%~1" == "mingwincygwin" (
+    SET INSTALLMODE=%~1
   ) ELSE (
-    IF "%1" == "absolute" (
-      SET INSTALLMODE=%1
+    IF "%~1" == "absolute" (
+      SET INSTALLMODE=%~1
     ) ELSE (
-      IF "%1" == "relocatable" (
-        SET INSTALLMODE=%1
+      IF "%~1" == "relocatable" (
+        SET INSTALLMODE=%~1
       ) ELSE (
         ECHO "Invalid -mode, valid are mingwincygwin, absolute and relocatable"
         GOTO :EOF
@@ -120,118 +122,124 @@ IF "%0" == "-mode" (
   GOTO Parse
 )
 
-IF "%0" == "-installer" (
-  SET MAKEINSTALLER=%1
+IF "%~0" == "-installer" (
+  SET MAKEINSTALLER=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-ocaml" (
-  SET INSTALLOCAML=%1
+IF "%~0" == "-ocaml" (
+  SET INSTALLOCAML=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-make" (
-  SET INSTALLMAKE=%1
+IF "%~0" == "-make" (
+  SET INSTALLMAKE=%~1
+  CALL :CheckYN -installer %~1 || GOTO ErrorExit
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-destcyg" (
-  SET DESTCYG=%1
+IF "%~0" == "-destcyg" (
+  SET DESTCYG=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-destcoq" (
-  SET DESTCOQ=%1
+IF "%~0" == "-destcoq" (
+  SET DESTCOQ=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-setup" (
-  SET SETUP=%1
+IF "%~0" == "-setup" (
+  SET SETUP=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-proxy" (
-  SET PROXY="%1"
+IF "%~0" == "-proxy" (
+  SET PROXY=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-cygrepo" (
-  SET CYGWIN_REPOSITORY="%1"
+IF "%~0" == "-cygrepo" (
+  SET CYGWIN_REPOSITORY=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-cygcache" (
-  SET CYGWIN_LOCAL_CACHE_WFMT="%1"
+IF "%~0" == "-cygcache" (
+  SET CYGWIN_LOCAL_CACHE_WFMT=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-cyglocal" (
-  SET CYGWIN_FROM_CACHE=%1
+IF "%~0" == "-cyglocal" (
+  SET CYGWIN_FROM_CACHE=%~1
+  CALL :CheckYN -cyglocal %~1 || GOTO ErrorExit
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-cygquiet" (
-  SET CYGWIN_QUIET=%1
+IF "%~0" == "-cygquiet" (
+  SET CYGWIN_QUIET=%~1
+  CALL :CheckYN -cygquiet %~1 || GOTO ErrorExit
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-srccache" (
-  SET SOURCE_LOCAL_CACHE_WFMT="%1"
+IF "%~0" == "-srccache" (
+  SET SOURCE_LOCAL_CACHE_WFMT=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-coqver" (
-  SET COQ_VERSION=%1
+IF "%~0" == "-coqver" (
+  SET COQ_VERSION=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-gtksrc" (
-  SET GTK_FROM_SOURCES=%1
+IF "%~0" == "-gtksrc" (
+  SET GTK_FROM_SOURCES=%~1
+  CALL :CheckYN -gtksrc %~1 || GOTO ErrorExit
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF "%0" == "-threads" (
-  SET MAKE_THREADS=%1
+IF "%~0" == "-threads" (
+  SET MAKE_THREADS=%~1
   SHIFT
   SHIFT
   GOTO Parse
 )
 
-IF NOT "%0" == "" (
+IF NOT "%~0" == "" (
   ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW
-  ECHO !!! Illegal parameter %0
+  ECHO !!! Illegal parameter %~0
   ECHO Usage: 
   ECHO MakeCoq_MinGW
   CALL :PrintPars
-  goto :EOF
+  GOTO :EOF
 )
 
 IF NOT EXIST %SETUP% (
@@ -255,7 +263,7 @@ 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)
+IF "%COQREGTESTING%"=="Y" (GOTO DontAsk)
   SET /p ANSWER=Is this correct? y/n 
   IF NOT "%ANSWER%"=="y" (GOTO :EOF)
 :DontAsk
@@ -325,7 +333,7 @@ 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
+if exist "%LOGFILE%" GOTO logfileloop
 
 REM Run Cygwin Setup
 
@@ -339,10 +347,10 @@ IF NOT "%CYGWIN_QUIET%" == "Y" (
 
 IF "%RUNSETUP%"=="Y" (
   %SETUP% ^
-    --proxy %PROXY% ^
-    --site %CYGWIN_REPOSITORY% ^
-    --root %CYGWIN_INSTALLDIR_WFMT% ^
-    --local-package-dir %CYGWIN_LOCAL_CACHE_WFMT% ^
+    --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 ^
@@ -359,11 +367,11 @@ IF "%RUNSETUP%"=="Y" (
     -P libtool,automake ^
     -P intltool ^
     > "%LOGFILE%" ^
-    || GOTO :Error
+    || GOTO ErrorExit
 
-  MKDIR %CYGWIN_INSTALLDIR_WFMT%\build
-  MKDIR %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs
-  MOVE  "%LOGFILE%" %CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log || GOTO :Error
+  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build"
+  MKDIR "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs"
+  MOVE  "%LOGFILE%" "%CYGWIN_INSTALLDIR_WFMT%\build\buildlogs\cygwinsetup.log" || GOTO ErrorExit
 )
 
 
@@ -377,18 +385,18 @@ IF NOT "%CYGWIN_QUIET%" == "Y" (
 
 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
+copy "%BATCHDIR%\configure_profile.sh" "%CYGWIN_INSTALLDIR_WFMT%\var\tmp" || GOTO ErrorExit
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\var\tmp\configure_profile.sh" "%PROXY%" || GOTO ErrorExit
 
 ECHO ========== BUILD COQ ==========
 
-MKDIR %CYGWIN_INSTALLDIR_WFMT%\build
-MKDIR %CYGWIN_INSTALLDIR_WFMT%\build\patches
+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
+COPY "%BATCHDIR%\makecoq_mingw.sh" "%CYGWIN_INSTALLDIR_WFMT%\build" || GOTO ErrorExit
+COPY "%BATCHDIR%\patches_coq\*.*" "%CYGWIN_INSTALLDIR_WFMT%\build\patches" || GOTO ErrorExit
 
-%BASH% --login %CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh || GOTO :Error
+%BASH% --login "%CYGWIN_INSTALLDIR_CFMT%\build\makecoq_mingw.sh" || GOTO ErrorExit
 
 ECHO ========== FINISHED ==========
 
@@ -440,6 +448,19 @@ ECHO ========== BATCH FUNCTIONS ==========
   ECHO -threads  = %MAKE_THREADS%
   GOTO :EOF
 
-:Error
-ECHO Building Coq failed with error code %errorlevel%
-EXIT /b %errorlevel%
+:CheckYN
+  REM Reset errorlevel to 0
+  CMD /c "EXIT /b 0"
+  IF "%2" == "Y" (
+    REM OK Y
+  ) ELSE IF "%2" == "N" (
+    REM OK N
+  ) ELSE (
+    ECHO ERROR Parameter %1 must be Y or N, but is %2
+    GOTO ErrorExit
+  )
+  GOTO :EOF
+
+:ErrorExit
+  ECHO ERROR MakeCoq_MinGW.bat failed
+  EXIT /b 1
diff --git a/dev/build/windows/MakeCoq_SetRootPath.bat b/dev/build/windows/MakeCoq_SetRootPath.bat
index 3a3711724..bcb104772 100644
--- a/dev/build/windows/MakeCoq_SetRootPath.bat
+++ b/dev/build/windows/MakeCoq_SetRootPath.bat
@@ -1,3 +1,14 @@
+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 ========== CHOOSE A SENSIBLE ROOT PATH ==========
+
 @ ECHO OFF
 
 REM Figure out a root path for coq and cygwin
diff --git a/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat b/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat
new file mode 100755
index 000000000..d7d3c5b9d
--- /dev/null
+++ b/dev/build/windows/MakeCoq_explicitcachefolders_installer.bat
@@ -0,0 +1,28 @@
+@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 ========== BUILD COQ ==========

+

+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -installer=Y ^

+  -coqver=git-v8.6 ^

+  -destcyg="%ROOTPATH%\cygwin_coq64_cachefolder_inst" ^

+  -destcoq="%ROOTPATH%\coq64_cachefolder_inst" ^

+  -cygcache="%ROOTPATH%\cache\cygwin" ^

+  -srccache="%ROOTPATH%\cache\source"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_explicitcachefolders_installer.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_local_installer.bat b/dev/build/windows/MakeCoq_local_installer.bat
new file mode 100755
index 000000000..752b73c10
--- /dev/null
+++ b/dev/build/windows/MakeCoq_local_installer.bat
@@ -0,0 +1,26 @@
+@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 ========== BUILD COQ ==========

+

+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -installer=Y ^

+  -coqver=/cygdrive/d/coqgit/coq-8.6 ^

+  -destcyg="%ROOTPATH%\cygwin_coq64_local_inst" ^

+  -destcoq="%ROOTPATH%\coq64_local_inst"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_local_installer.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat
index 2b0b83fed..7b17e721b 100644
--- a/dev/build/windows/MakeCoq_regtest_noproxy.bat
+++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat
@@ -1,7 +1,18 @@
+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 ========== BUILD COQ ==========

+

 call MakeCoq_SetRootPath

 

 SET HTTP_PROXY=

-EXPORT HTTP_PROXY=

+SET HTTPS_PROXY=

 MKDIR C:\Temp\srccache

 

 call MakeCoq_MinGW.bat ^

diff --git a/dev/build/windows/MakeCoq_regtests.bat b/dev/build/windows/MakeCoq_regtests.bat
index 6e36d0140..74c26456b 100644
--- a/dev/build/windows/MakeCoq_regtests.bat
+++ b/dev/build/windows/MakeCoq_regtests.bat
@@ -1,16 +1,36 @@
-SET COQREGTESTING=Y
+REM ========== COPYRIGHT/COPYLEFT ==========
 
-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 (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 ========== RUN REGRESSION TESTS FOR COQ BUILD SCRIPTS ==========
+
+SET COQREGTESTING=Y
 
 REM Current stable
-call MakeCoq_85pl3_abs_ocaml.bat
-call MakeCoq_85pl3_installer.bat
-call MakeCoq_85pl3_installer_32.bat
+call MakeCoq_86git_abs_ocaml.bat || GOTO Error
+call MakeCoq_86git_installer.bat || GOTO Error
+call MakeCoq_86git_installer_32.bat || GOTO Error
 
 REM Old but might still be used
-call MakeCoq_85pl2_abs_ocaml.bat
-call MakeCoq_84pl6_abs_ocaml.bat
+call MakeCoq_85pl3_abs_ocaml.bat || GOTO Error
+call MakeCoq_84pl6_abs_ocaml.bat || GOTO Error
+
+REM Special variants, e.g. for debugging
+call MakeCoq_86git_abs_ocaml_gtksrc.bat || GOTO Error
+call MakeCoq_local_installer.bat || GOTO Error
+call MakeCoq_explicitcachefolders_installer.bat || GOTO Error
+
+REM Bleeding edge
+call MakeCoq_trunk_installer.bat || GOTO Error
+
+ECHO MakeCoq_regtests.bat: All tests finished successfully
+GOTO :EOF
+
+:Error
+ECHO MakeCoq_regtests.bat failed with error code %ERRORLEVEL%
+EXIT /b %ERRORLEVEL%
diff --git a/dev/build/windows/MakeCoq_trunk_installer.bat b/dev/build/windows/MakeCoq_trunk_installer.bat
new file mode 100755
index 000000000..f4f582732
--- /dev/null
+++ b/dev/build/windows/MakeCoq_trunk_installer.bat
@@ -0,0 +1,26 @@
+@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 ========== BUILD COQ ==========

+

+call MakeCoq_SetRootPath

+

+call MakeCoq_MinGW.bat ^

+  -arch=64 ^

+  -installer=Y ^

+  -coqver=git-trunk ^

+  -destcyg="%ROOTPATH%\cygwin_coq64_trunk_inst" ^

+  -destcoq="%ROOTPATH%\coq64_trunk_inst"

+

+IF %ERRORLEVEL% NEQ 0 (

+  ECHO MakeCoq_86git_installer.bat failed with error code %ERRORLEVEL%

+  EXIT /b %ERRORLEVEL%

+)

diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt
index 0faf5bc53..a6d8e4462 100644
--- a/dev/build/windows/ReadMe.txt
+++ b/dev/build/windows/ReadMe.txt
@@ -1,3 +1,12 @@
+(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
+
+This license also applies to all files in the patches_coq subfolder.
+
 ==================== Purpose / Goal ====================
 
 The main purpose of these scripts is to build Coq for Windows in a reproducible
@@ -286,9 +295,16 @@ Default value: <folder of MakeCoq_MinGW.bat>\source_cache
 
 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.
+Possible values: 8.4pl6, 8.5pl2, 8.5pl3, 8.6
+                 (download from https://coq.inria.fr/distrib/V$COQ_VERSION/files/coq-<version>.tar.gz)
+                 Others versions might work, but are untested.
                  8.4 is only tested in mode=absoloute
+                 
+                 git-v8.6, git-trunk
+                 (download from https://github.com/coq/coq/archive/<version without git->.zip)
+                 
+                 /cygdrive/....
+                 Use local folder. The sources are archived as coq-local.tar.gz
 
 Default value: 8.5pl3
 
@@ -322,6 +338,8 @@ Possible values: 1..N.
 
 ==================== TODO ====================
 
+- Check for spaces in destination paths
+- Check for = signs in all paths (DOS commands don't work with pathes with = in it, possibly even when quoted)
 - 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)
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 09a9cf35a..0b61a31e7 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -1,5 +1,16 @@
 #!/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
+
+###################### CONFIGURE CYGWIN USER PROFILE FOR BUILDING COQ ######################
+
 rcfile=~/.bash_profile
 donefile=~/.bash_profile.upated
 
@@ -7,7 +18,7 @@ if [ ! -f $donefile ] ; then
 
     echo >> $rcfile
     
-    if [ -n "$1" ]; then
+    if [ "$1" != "" -a "$1" != " " ]; then
       echo export http_proxy="http://$1" >> $rcfile
       echo export https_proxy="http://$1" >> $rcfile
       echo export ftp_proxy="http://$1" >> $rcfile
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
index 65278d5c9..cbcf14ec2 100644
--- a/dev/build/windows/difftar-folder.sh
+++ b/dev/build/windows/difftar-folder.sh
@@ -8,35 +8,28 @@
 # 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 ######################
+###################### DIFF A TAR FILE AND A FOLDER ######################
 
 set -o nounset
 
 # Print usage
 
-if [ "$#" -lt 1 ] ; then
+if [ "$#" -lt 2 ] ; 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.'
+  echo 'difftar-folder.sh <tarfile> <folder> [strip]'
+  echo '<tarfile> is the name of the tar file do diff with (required)'
+  echo '<folder> is the name of the folder to diff with (required)'
+  echo '<strip> is the number of path components to strip from tar file (default is 0)'
+  echo 'All files in the tar file must have at least <strip> path components.'
+  echo 'This also adds new files from folder.new, if folder.new exists'
   exit 1
 fi
 
 # Parse parameters
 
 tarfile=$1
-
-if [ "$#" -ge 2 ] ; then
-  folder=$2
-else
-  folder=.
-fi
+folder=$2
 
 if [ "$#" -ge 3 ] ; then
   strip=$3
@@ -47,27 +40,33 @@ fi
 # Get path prefix if --strip is used
 
 if [ "$strip" -gt 0 ] ; then
-  prefix=`tar -t -f $tarfile | head -1`
+  # Get the path/name of the first file from teh tar and extract the first $strip path components
+  # This assumes that the first file in the tar file has at least $strip many path components
+  prefix=$(tar -t -f $tarfile | head -1 | cut -d / -f -$strip)/
 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
+orig=$folder.orig
 mkdir -p "$orig"
 
+# New amd empty filefolder
+
+new=$folder.new
+empty=$folder.empty
+mkdir -p "$empty"
+
+# Print information (this is ignored by patch)
+
+echo diff/patch file created on $(date) with:
+echo difftar-folder.sh $@
+echo TARFILE=    $tarfile
+echo FOLDER=     $folder
+echo TARSTRIP=   $strip
+echo TARPREFIX=  $prefix
+echo ORIGFOLDER= $orig
 
 # Make sure tar uses english output (for Mod time differs)
 export LC_ALL=C
@@ -83,4 +82,8 @@ tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod tim
     # Compute diff
     diff -u "$orig/$file" "$folder/$file" 
   fi
-done
\ No newline at end of file
+done
+
+if [ -d "$new" ] ; then
+  diff -u -r --unidirectional-new-file $empty $new
+fi
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 98e80c765..e17923951 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -98,6 +98,8 @@ mkdir -p $TARBALLS
 mkdir -p $FILELISTS
 cd /build
 
+# Create source cache folder
+mkdir -p "$SOURCE_LOCAL_CACHE_CFMT"
 
 # sysroot prefix for the above /build/host/target combination
 PREFIX=$CYGWIN_INSTALLDIR_MFMT/usr/$TARGET_ARCH/sys-root/mingw
@@ -112,9 +114,9 @@ else
   PREFIXOCAML=$PREFIX
 fi
 
-mkdir -p $PREFIX/bin
-mkdir -p $PREFIXCOQ/bin
-mkdir -p $PREFIXOCAML/bin
+mkdir -p "$PREFIX/bin"
+mkdir -p "$PREFIXCOQ/bin"
+mkdir -p "$PREFIXOCAML/bin"
 
 ###################### Copy Cygwin Setup Info #####################
 
@@ -128,7 +130,7 @@ 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 "$CYGWIN_LOCAL_CACHE_WFMT/$CYGWIN_REPO_FOLDER/$CYGWINARCH/setup.ini" $TARBALLS
 cp /etc/setup/installed.db $TARBALLS
   
 ###################### LOGGING #####################
@@ -158,6 +160,21 @@ logn() {
   "$@" > $LOGS/$LOGTARGET-$LOGTARGETEX.log 2> $LOGS/$LOGTARGET-$LOGTARGETEX.err
 }
  
+###################### 'UNFIX' SED #####################
+
+# In Cygwin SED used to do CR-LF to LF conversion, but since sed 4.4-1 this was changed
+# We replace sed with a shell script which restores the old behavior for piped input
+
+#if [ -f /bin/sed.exe ]
+#then
+#  mv /bin/sed.exe /bin/sed_orig.exe
+#fi
+#cat  > /bin/sed << EOF
+##!/bin/sh
+#dos2unix | /bin/sed_orig.exe "$@"
+#EOF
+#chmod a+x /bin/sed
+
 ###################### UTILITY FUNCTIONS #####################
 
 # ------------------------------------------------------------------------------
@@ -202,8 +219,8 @@ function get_expand_source_tar {
   
   # 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
+    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
@@ -211,8 +228,8 @@ function get_expand_source_tar {
       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
+      if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then
+        cp $TARBALLS/$name.$3 "$SOURCE_LOCAL_CACHE_CFMT"
       fi
     fi
   fi
@@ -341,7 +358,7 @@ function build_post {
 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}"
+    logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" "${@:5}"
     log1 make $MAKE_OPT
     log2 make install
     log2 make clean
@@ -388,7 +405,7 @@ function install_rec {
 
 function list_files {
   if [ ! -e "/build/filelists/$1" ] ; then
-    ( cd $PREFIXCOQ && find -type f | sort > /build/filelists/$1 )
+    ( cd "$PREFIXCOQ" && find -type f | sort > /build/filelists/$1 )
   fi
 }
 
@@ -436,6 +453,18 @@ function files_to_nsis {
 
 ###################### MODULE BUILD FUNCTIONS #####################
 
+##### SED #####
+
+function make_sed {
+  if build_prep https://ftp.gnu.org/gnu/sed/  sed-4.2.2  tar.gz ; then
+    logn configure ./configure
+    log1 make
+    log2 make install
+    log2 make clean
+    build_post
+  fi
+}
+
 ##### LIBPNG #####
 
 function make_libpng {
@@ -639,9 +668,9 @@ function make_libxml2 {
   # 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
+    # ./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
+    ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --without-python
     log1 make $MAKE_OPT all
     log2 make install
     log2 make clean
@@ -676,10 +705,10 @@ 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
+    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
+    cp flexdll*_mingw64.o "$PREFIXOCAML/bin"
   else
     echo "Unknown target architecture"
     return 1
@@ -691,7 +720,7 @@ function install_flexdll {
 function install_flexlink {
   cp flexlink.exe /usr/$TARGET_ARCH/bin
     
-  cp flexlink.exe $PREFIXOCAML/bin
+  cp flexlink.exe "$PREFIXOCAML/bin"
 }
 
 # Get binary flexdll flexlink for building OCaml
@@ -737,7 +766,7 @@ function make_ln {
     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
+    install -D ln.exe "$PREFIXCOQ/bin/ln.exe"
     cd ..
     touch flagfiles/myln.finished
   fi
@@ -762,6 +791,7 @@ function make_ocaml {
     fi
 
     # Prefix is fixed in make file - replace it with the real one
+    # TODO: this might not work if PREFIX contains spaces
     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
@@ -782,15 +812,15 @@ function make_ocaml {
     
     # Move license files and other into into special folder
     if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-      mkdir -p $PREFIXOCAML/license_readme/ocaml
+      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
+      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
@@ -798,12 +828,28 @@ function make_ocaml {
   make_flex_dll_link
 }
 
+##### OCAML EXTRA TOOLS #####
+
+function make_ocaml_tools {
+  make_findlib
+  make_menhir
+  make_camlp5
+}
+
+##### OCAML EXTRA LIBRARIES #####
+
+function make_ocaml_libs {
+  make_findlib
+  make_lablgtk
+  make_stdint
+}
+
 ##### 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
+    logn configure ./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
@@ -824,9 +870,9 @@ function make_menhir {
   # 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
+    log2 make all PREFIX="$PREFIXOCAML"
+    log2 make install PREFIX="$PREFIXOCAML"
+    mv "$PREFIXOCAML/bin/menhir" "$PREFIXOCAML/bin/menhir.exe"
     build_post
   fi
 }
@@ -863,7 +909,7 @@ function make_camlp5 {
     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/
+    cp lib/gramlib.a "$PREFIXOCAML/libocaml/camlp5/"
     log2 make clean
     build_post
   fi
@@ -878,11 +924,13 @@ function make_camlp5 {
 function make_lablgtk {
   make_ocaml
   make_findlib
-  make_camlp4
+  make_camlp4 # required by lablgtk-2.18.3 and lablgtk-2.18.5
+  make_gtk2
+  make_gtk_sourceview2
   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
+    logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXOCAML"
     
     # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
     
@@ -920,7 +968,7 @@ function make_stdint {
 
 function copy_coq_dll {
   if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
-    cp /usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1 $PREFIXCOQ/bin/$1
+    cp /usr/${ARCH}-w64-mingw32/sys-root/mingw/bin/$1 "$PREFIXCOQ/bin/$1"
   fi
 }
 
@@ -954,6 +1002,7 @@ function copy_coq_dlls {
   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 libpcre-1.dll
   copy_coq_dll LIBPIXMAN-1-0.DLL
   copy_coq_dll LIBPNG16-16.DLL
   copy_coq_dll LIBXML2-2.DLL
@@ -962,7 +1011,6 @@ function copy_coq_dlls {
   # 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
@@ -986,13 +1034,13 @@ function copy_coq_dlls {
 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 
+    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
 }
@@ -1000,23 +1048,23 @@ function copy_coq_objects {
 # 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
+  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
+    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
+      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
+    mkdir -p "$PREFIXCOQ/ide"
+    mv "$PREFIXCOQ/share/coq/"*.png  "$PREFIXCOQ/ide"
+    rmdir "$PREFIXCOQ/share/coq"
   fi
 }
 
@@ -1024,16 +1072,17 @@ function copq_coq_gtk {
 
 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
+    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.win                     "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || 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
 }
 
@@ -1043,19 +1092,38 @@ function make_coq {
   make_ocaml
   make_lablgtk
   make_camlp5
-  if 
+  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 ;;
+      # e.g. git-v8.6 => download from https://github.com/coq/coq/archive/v8.6.zip
+      # e.g. git-trunk => download from https://github.com/coq/coq/archive/trunk.zip
+      git-*) 
+        COQ_BUILD_PATH=/build/coq-${COQ_VERSION}
+        build_prep https://github.com/coq/coq/archive ${COQ_VERSION##git-} zip 1 coq-${COQ_VERSION}
+        ;;
+      
+      # e.g. /cygdrive/d/coqgit
+      /*)
+        # Todo: --exclude-vcs-ignores doesn't work because tools/coqdoc/coqdoc.sty is excluded => fix .gitignore
+        # But this is not a big deal, only 2 files are removed with --exclude-vcs-ignores from a fresch clone
+        COQ_BUILD_PATH=/build/coq-local
+        tar -zcf $TARBALLS/coq-local.tar.gz --exclude-vcs -C "${COQ_VERSION%/*}" "${COQ_VERSION##*/}"
+        build_prep NEVER-DOWNLOADED coq-local tar.gz
+        ;;
+      
+      # e.g. 8.6 => https://coq.inria.fr/distrib/8.6/files/coq-8.6.tar.gz
+      *)
+        COQ_BUILD_PATH=/build/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
+      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
+      logn configure ./configure -debug -with-doc no -prefix "$PREFIXCOQ"
     fi
 
     # The windows resource compiler binary name is hard coded
@@ -1070,7 +1138,7 @@ function make_coq {
     fi
     
     if [ "$INSTALLMODE" == "relocatable" ]; then
-      ./configure -debug -with-doc no -prefix $PREFIXCOQ -libdir $PREFIXCOQ/lib -mandir $PREFIXCOQ/man
+      logn reconfigure ./configure -debug -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
     fi
 
     log2 make install
@@ -1101,7 +1169,7 @@ function make_mingw_make {
     # 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
+    cp GccRel/gnumake.exe "$PREFIXCOQ/bin/make.exe"
     build_post
   fi
 }
@@ -1110,7 +1178,7 @@ function make_mingw_make {
 
 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-
+    logn configure ./configure --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIXCOQ" --program-prefix=$TARGET-
     log1 make $MAKE_OPT
     log2 make install
     # log2 make clean
@@ -1133,15 +1201,15 @@ function make_gcc {
     # 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
+    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 \
+        --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
+        # --with-sysroot="$PREFIX"  results in configure error that this is not an absolute path
     log1 make $MAKE_OPT
     log2 make install
     # log2 make clean
@@ -1176,14 +1244,14 @@ function get_cygwin_mingw_sources {
 
       # 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
+        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
+          if [ -d "$SOURCE_LOCAL_CACHE_CFMT" ] ; then
+            cp $TARBALLS/$SOURCEFILE "$SOURCE_LOCAL_CACHE_CFMT"
           fi
         fi
       fi
@@ -1199,7 +1267,7 @@ function get_cygwin_mingw_sources {
 function make_coq_installer {
   make_coq
   make_mingw_make
-  get_cygwin_mingw_sources
+  # 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
@@ -1230,14 +1298,14 @@ function make_coq_installer {
     NSIS=`pwd`/makensis.exe
     chmod u+x "$NSIS"
     # Change to Coq folder
-    cd ../coq-${COQ_VERSION}
+    cd $COQ_BUILD_PATH
     # 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`
+    VERSION=`grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r'`
     cd dev/nsis
-    logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH=$PREFIXCOQ -DCOQ_ICON=..\\..\\ide\\coq.ico coq_new.nsi
+    logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico coq_new.nsi
     
     build_post
   fi
@@ -1245,17 +1313,13 @@ function make_coq_installer {
 
 ###################### TOP LEVEL BUILD #####################
 
-make_gtk2
-make_gtk_sourceview2
-
+make_sed
 make_ocaml
-make_findlib
-make_lablgtk
-make_camlp4
-make_camlp5
-make_menhir
-make_stdint
+make_ocaml_tools
+make_ocaml_libs
+
 list_files ocaml
+
 make_coq
 
 if [ "$INSTALLMAKE" == "Y" ] ; then
diff --git a/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch b/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch
new file mode 100755
index 000000000..d210a0415
--- /dev/null
+++ b/dev/build/windows/patches_coq/sed-4.2.2-3.src.patch
@@ -0,0 +1,1301 @@
+--- origsrc/sed-4.2.2/doc/sed.1	2012-12-22 15:27:13.000000000 +0100
++++ src/sed-4.2.2/doc/sed.1	2013-06-27 18:10:47.974060492 +0200
+@@ -1,5 +1,5 @@
+ .\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.28.
+-.TH SED "1" "December 2012" "sed 4.2.2" "User Commands"
++.TH SED "1" "June 2013" "sed 4.2.2" "User Commands"
+ .SH NAME
+ sed \- stream editor for filtering and transforming text
+ .SH SYNOPSIS
+@@ -40,6 +40,10 @@ follow symlinks when processing in place
+ .IP
+ edit files in place (makes backup if SUFFIX supplied)
+ .HP
++\fB\-b\fR, \fB\-\-binary\fR
++.IP
++open files in binary mode (CR+LFs are not processed specially)
++.HP
+ \fB\-l\fR N, \fB\-\-line\-length\fR=\fIN\fR
+ .IP
+ specify the desired line-wrap length for the `l' command
+--- origsrc/sed-4.2.2/lib/regcomp.c	2012-12-22 14:21:52.000000000 +0100
++++ src/sed-4.2.2/lib/regcomp.c	2013-06-27 18:05:27.044448044 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ static reg_errcode_t re_compile_internal (regex_t *preg, const char * pattern,
+ 					  size_t length, reg_syntax_t syntax);
+@@ -95,20 +94,20 @@ static reg_errcode_t build_charclass (RE
+ 				      bitset_t sbcset,
+ 				      re_charset_t *mbcset,
+ 				      Idx *char_class_alloc,
+-				      const unsigned char *class_name,
++				      const char *class_name,
+ 				      reg_syntax_t syntax);
+ #else  /* not RE_ENABLE_I18N */
+ static reg_errcode_t build_equiv_class (bitset_t sbcset,
+ 					const unsigned char *name);
+ static reg_errcode_t build_charclass (RE_TRANSLATE_TYPE trans,
+ 				      bitset_t sbcset,
+-				      const unsigned char *class_name,
++				      const char *class_name,
+ 				      reg_syntax_t syntax);
+ #endif /* not RE_ENABLE_I18N */
+ static bin_tree_t *build_charclass_op (re_dfa_t *dfa,
+ 				       RE_TRANSLATE_TYPE trans,
+-				       const unsigned char *class_name,
+-				       const unsigned char *extra,
++				       const char *class_name,
++				       const char *extra,
+ 				       bool non_match, reg_errcode_t *err);
+ static bin_tree_t *create_tree (re_dfa_t *dfa,
+ 				bin_tree_t *left, bin_tree_t *right,
+@@ -293,7 +292,7 @@ weak_alias (__re_compile_fastmap, re_com
+ #endif
+ 
+ static inline void
+-__attribute ((always_inline))
++__attribute__ ((always_inline))
+ re_set_fastmap (char *fastmap, bool icase, int ch)
+ {
+   fastmap[ch] = 1;
+@@ -587,7 +586,7 @@ weak_alias (__regerror, regerror)
+ static const bitset_t utf8_sb_map =
+ {
+   /* Set the first 128 bits.  */
+-# ifdef __GNUC__
++# if defined __GNUC__ && !defined __STRICT_ANSI__
+   [0 ... 0x80 / BITSET_WORD_BITS - 1] = BITSET_WORD_MAX
+ # else
+ #  if 4 * BITSET_WORD_BITS < ASCII_CHARS
+@@ -664,7 +663,10 @@ regfree (preg)
+ {
+   re_dfa_t *dfa = preg->buffer;
+   if (BE (dfa != NULL, 1))
+-    free_dfa_content (dfa);
++    {
++      lock_fini (dfa->lock);
++      free_dfa_content (dfa);
++    }
+   preg->buffer = NULL;
+   preg->allocated = 0;
+ 
+@@ -785,6 +787,8 @@ re_compile_internal (regex_t *preg, cons
+   preg->used = sizeof (re_dfa_t);
+ 
+   err = init_dfa (dfa, length);
++  if (BE (err == REG_NOERROR && lock_init (dfa->lock) != 0, 0))
++    err = REG_ESPACE;
+   if (BE (err != REG_NOERROR, 0))
+     {
+       free_dfa_content (dfa);
+@@ -798,8 +802,6 @@ re_compile_internal (regex_t *preg, cons
+   strncpy (dfa->re_str, pattern, length + 1);
+ #endif
+ 
+-  __libc_lock_init (dfa->lock);
+-
+   err = re_string_construct (&regexp, pattern, length, preg->translate,
+ 			     (syntax & RE_ICASE) != 0, dfa);
+   if (BE (err != REG_NOERROR, 0))
+@@ -807,6 +809,7 @@ re_compile_internal (regex_t *preg, cons
+     re_compile_internal_free_return:
+       free_workarea_compile (preg);
+       re_string_destruct (&regexp);
++      lock_fini (dfa->lock);
+       free_dfa_content (dfa);
+       preg->buffer = NULL;
+       preg->allocated = 0;
+@@ -839,6 +842,7 @@ re_compile_internal (regex_t *preg, cons
+ 
+   if (BE (err != REG_NOERROR, 0))
+     {
++      lock_fini (dfa->lock);
+       free_dfa_content (dfa);
+       preg->buffer = NULL;
+       preg->allocated = 0;
+@@ -954,10 +958,10 @@ static void
+ internal_function
+ init_word_char (re_dfa_t *dfa)
+ {
+-  dfa->word_ops_used = 1;
+   int i = 0;
+   int j;
+   int ch = 0;
++  dfa->word_ops_used = 1;
+   if (BE (dfa->map_notascii == 0, 1))
+     {
+       bitset_word_t bits0 = 0x00000000;
+@@ -2423,8 +2427,8 @@ parse_expression (re_string_t *regexp, r
+     case OP_WORD:
+     case OP_NOTWORD:
+       tree = build_charclass_op (dfa, regexp->trans,
+-				 (const unsigned char *) "alnum",
+-				 (const unsigned char *) "_",
++				 "alnum",
++				 "_",
+ 				 token->type == OP_NOTWORD, err);
+       if (BE (*err != REG_NOERROR && tree == NULL, 0))
+ 	return NULL;
+@@ -2432,8 +2436,8 @@ parse_expression (re_string_t *regexp, r
+     case OP_SPACE:
+     case OP_NOTSPACE:
+       tree = build_charclass_op (dfa, regexp->trans,
+-				 (const unsigned char *) "space",
+-				 (const unsigned char *) "",
++				 "space",
++				 "",
+ 				 token->type == OP_NOTSPACE, err);
+       if (BE (*err != REG_NOERROR && tree == NULL, 0))
+ 	return NULL;
+@@ -2713,7 +2717,6 @@ build_range_exp (const reg_syntax_t synt
+     wchar_t wc;
+     wint_t start_wc;
+     wint_t end_wc;
+-    wchar_t cmp_buf[6] = {L'\0', L'\0', L'\0', L'\0', L'\0', L'\0'};
+ 
+     start_ch = ((start_elem->type == SB_CHAR) ? start_elem->opr.ch
+ 		: ((start_elem->type == COLL_SYM) ? start_elem->opr.name[0]
+@@ -2727,11 +2730,7 @@ build_range_exp (const reg_syntax_t synt
+ 	      ? __btowc (end_ch) : end_elem->opr.wch);
+     if (start_wc == WEOF || end_wc == WEOF)
+       return REG_ECOLLATE;
+-    cmp_buf[0] = start_wc;
+-    cmp_buf[4] = end_wc;
+-
+-    if (BE ((syntax & RE_NO_EMPTY_RANGES)
+-            && wcscoll (cmp_buf, cmp_buf + 4) > 0, 0))
++    else if (BE ((syntax & RE_NO_EMPTY_RANGES) && start_wc > end_wc, 0))
+       return REG_ERANGE;
+ 
+     /* Got valid collation sequence values, add them as a new entry.
+@@ -2772,9 +2771,7 @@ build_range_exp (const reg_syntax_t synt
+     /* Build the table for single byte characters.  */
+     for (wc = 0; wc < SBC_MAX; ++wc)
+       {
+-	cmp_buf[2] = wc;
+-	if (wcscoll (cmp_buf, cmp_buf + 2) <= 0
+-	    && wcscoll (cmp_buf + 2, cmp_buf + 4) <= 0)
++	if (start_wc <= wc && wc <= end_wc)
+ 	  bitset_set (sbcset, wc);
+       }
+   }
+@@ -2843,40 +2840,29 @@ parse_bracket_exp (re_string_t *regexp,
+ 
+   /* Local function for parse_bracket_exp used in _LIBC environment.
+      Seek the collating symbol entry corresponding to NAME.
+-     Return the index of the symbol in the SYMB_TABLE.  */
++     Return the index of the symbol in the SYMB_TABLE,
++     or -1 if not found.  */
+ 
+   auto inline int32_t
+-  __attribute ((always_inline))
+-  seek_collating_symbol_entry (name, name_len)
+-	 const unsigned char *name;
+-	 size_t name_len;
+-    {
+-      int32_t hash = elem_hash ((const char *) name, name_len);
+-      int32_t elem = hash % table_size;
+-      if (symb_table[2 * elem] != 0)
+-	{
+-	  int32_t second = hash % (table_size - 2) + 1;
+-
+-	  do
+-	    {
+-	      /* First compare the hashing value.  */
+-	      if (symb_table[2 * elem] == hash
+-		  /* Compare the length of the name.  */
+-		  && name_len == extra[symb_table[2 * elem + 1]]
+-		  /* Compare the name.  */
+-		  && memcmp (name, &extra[symb_table[2 * elem + 1] + 1],
+-			     name_len) == 0)
+-		{
+-		  /* Yep, this is the entry.  */
+-		  break;
+-		}
++  __attribute__ ((always_inline))
++  seek_collating_symbol_entry (const unsigned char *name, size_t name_len)
++    {
++      int32_t elem;
+ 
+-	      /* Next entry.  */
+-	      elem += second;
+-	    }
+-	  while (symb_table[2 * elem] != 0);
+-	}
+-      return elem;
++      for (elem = 0; elem < table_size; elem++)
++	if (symb_table[2 * elem] != 0)
++	  {
++	    int32_t idx = symb_table[2 * elem + 1];
++	    /* Skip the name of collating element name.  */
++	    idx += 1 + extra[idx];
++	    if (/* Compare the length of the name.  */
++		name_len == extra[idx]
++		/* Compare the name.  */
++		&& memcmp (name, &extra[idx + 1], name_len) == 0)
++	      /* Yep, this is the entry.  */
++	      return elem;
++	  }
++      return -1;
+     }
+ 
+   /* Local function for parse_bracket_exp used in _LIBC environment.
+@@ -2884,9 +2870,8 @@ parse_bracket_exp (re_string_t *regexp,
+      Return the value if succeeded, UINT_MAX otherwise.  */
+ 
+   auto inline unsigned int
+-  __attribute ((always_inline))
+-  lookup_collation_sequence_value (br_elem)
+-	 bracket_elem_t *br_elem;
++  __attribute__ ((always_inline))
++  lookup_collation_sequence_value (bracket_elem_t *br_elem)
+     {
+       if (br_elem->type == SB_CHAR)
+ 	{
+@@ -2914,7 +2899,7 @@ parse_bracket_exp (re_string_t *regexp,
+ 	      int32_t elem, idx;
+ 	      elem = seek_collating_symbol_entry (br_elem->opr.name,
+ 						  sym_name_len);
+-	      if (symb_table[2 * elem] != 0)
++	      if (elem != -1)
+ 		{
+ 		  /* We found the entry.  */
+ 		  idx = symb_table[2 * elem + 1];
+@@ -2932,7 +2917,7 @@ parse_bracket_exp (re_string_t *regexp,
+ 		  /* Return the collation sequence value.  */
+ 		  return *(unsigned int *) (extra + idx);
+ 		}
+-	      else if (symb_table[2 * elem] == 0 && sym_name_len == 1)
++	      else if (sym_name_len == 1)
+ 		{
+ 		  /* No valid character.  Match it as a single byte
+ 		     character.  */
+@@ -2953,12 +2938,9 @@ parse_bracket_exp (re_string_t *regexp,
+      update it.  */
+ 
+   auto inline reg_errcode_t
+-  __attribute ((always_inline))
+-  build_range_exp (sbcset, mbcset, range_alloc, start_elem, end_elem)
+-	 re_charset_t *mbcset;
+-	 Idx *range_alloc;
+-	 bitset_t sbcset;
+-	 bracket_elem_t *start_elem, *end_elem;
++  __attribute__ ((always_inline))
++  build_range_exp (bitset_t sbcset, re_charset_t *mbcset, int *range_alloc,
++		   bracket_elem_t *start_elem, bracket_elem_t *end_elem)
+     {
+       unsigned int ch;
+       uint32_t start_collseq;
+@@ -2971,6 +2953,7 @@ parse_bracket_exp (re_string_t *regexp,
+ 	      0))
+ 	return REG_ERANGE;
+ 
++      /* FIXME: Implement rational ranges here, too.  */
+       start_collseq = lookup_collation_sequence_value (start_elem);
+       end_collseq = lookup_collation_sequence_value (end_elem);
+       /* Check start/end collation sequence values.  */
+@@ -3036,26 +3019,23 @@ parse_bracket_exp (re_string_t *regexp,
+      pointer argument since we may update it.  */
+ 
+   auto inline reg_errcode_t
+-  __attribute ((always_inline))
+-  build_collating_symbol (sbcset, mbcset, coll_sym_alloc, name)
+-	 re_charset_t *mbcset;
+-	 Idx *coll_sym_alloc;
+-	 bitset_t sbcset;
+-	 const unsigned char *name;
++  __attribute__ ((always_inline))
++  build_collating_symbol (bitset_t sbcset, re_charset_t *mbcset,
++			  Idx *coll_sym_alloc, const unsigned char *name)
+     {
+       int32_t elem, idx;
+       size_t name_len = strlen ((const char *) name);
+       if (nrules != 0)
+ 	{
+ 	  elem = seek_collating_symbol_entry (name, name_len);
+-	  if (symb_table[2 * elem] != 0)
++	  if (elem != -1)
+ 	    {
+ 	      /* We found the entry.  */
+ 	      idx = symb_table[2 * elem + 1];
+ 	      /* Skip the name of collating element name.  */
+ 	      idx += 1 + extra[idx];
+ 	    }
+-	  else if (symb_table[2 * elem] == 0 && name_len == 1)
++	  else if (name_len == 1)
+ 	    {
+ 	      /* No valid character, treat it as a normal
+ 		 character.  */
+@@ -3298,7 +3278,8 @@ parse_bracket_exp (re_string_t *regexp,
+ #ifdef RE_ENABLE_I18N
+ 				      mbcset, &char_class_alloc,
+ #endif /* RE_ENABLE_I18N */
+-				      start_elem.opr.name, syntax);
++				      (const char *) start_elem.opr.name,
++				      syntax);
+ 	      if (BE (*err != REG_NOERROR, 0))
+ 	       goto parse_bracket_exp_free_return;
+ 	      break;
+@@ -3578,14 +3559,14 @@ static reg_errcode_t
+ #ifdef RE_ENABLE_I18N
+ build_charclass (RE_TRANSLATE_TYPE trans, bitset_t sbcset,
+ 		 re_charset_t *mbcset, Idx *char_class_alloc,
+-		 const unsigned char *class_name, reg_syntax_t syntax)
++		 const char *class_name, reg_syntax_t syntax)
+ #else /* not RE_ENABLE_I18N */
+ build_charclass (RE_TRANSLATE_TYPE trans, bitset_t sbcset,
+-		 const unsigned char *class_name, reg_syntax_t syntax)
++		 const char *class_name, reg_syntax_t syntax)
+ #endif /* not RE_ENABLE_I18N */
+ {
+   int i;
+-  const char *name = (const char *) class_name;
++  const char *name = class_name;
+ 
+   /* In case of REG_ICASE "upper" and "lower" match the both of
+      upper and lower cases.  */
+@@ -3659,8 +3640,8 @@ build_charclass (RE_TRANSLATE_TYPE trans
+ 
+ static bin_tree_t *
+ build_charclass_op (re_dfa_t *dfa, RE_TRANSLATE_TYPE trans,
+-		    const unsigned char *class_name,
+-		    const unsigned char *extra, bool non_match,
++		    const char *class_name,
++		    const char *extra, bool non_match,
+ 		    reg_errcode_t *err)
+ {
+   re_bitset_ptr_t sbcset;
+--- origsrc/sed-4.2.2/lib/regex-quote.c	1970-01-01 01:00:00.000000000 +0100
++++ src/sed-4.2.2/lib/regex-quote.c	2013-06-27 18:05:27.081447884 +0200
+@@ -0,0 +1,216 @@
++/* Construct a regular expression from a literal string.
++   Copyright (C) 1995, 2010-2013 Free Software Foundation, Inc.
++   Written by Bruno Haible <haible@clisp.cons.org>, 2010.
++
++   This program is free software: you can redistribute it and/or modify
++   it under the terms of the GNU General Public License as published by
++   the Free Software Foundation; either version 3 of the License, or
++   (at your option) any later version.
++
++   This program is distributed in the hope that it will be useful,
++   but WITHOUT ANY WARRANTY; without even the implied warranty of
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
++   GNU General Public License for more details.
++
++   You should have received a copy of the GNU General Public License
++   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
++
++#include <config.h>
++
++/* Specification.  */
++#include "regex-quote.h"
++
++#include <string.h>
++
++#include "mbuiter.h"
++#include "xalloc.h"
++
++/* Characters that are special in a BRE.  */
++static const char bre_special[] = "$^.*[]\\";
++
++/* Characters that are special in an ERE.  */
++static const char ere_special[] = "$^.*[]\\+?{}()|";
++
++struct regex_quote_spec
++regex_quote_spec_posix (int cflags, bool anchored)
++{
++  struct regex_quote_spec result;
++
++  strcpy (result.special, cflags != 0 ? ere_special : bre_special);
++  result.multibyte = true;
++  result.anchored = anchored;
++
++  return result;
++}
++
++/* Syntax bit values, defined in GNU <regex.h>.  We don't include it here,
++   otherwise this module would need to depend on gnulib module 'regex'.  */
++#define RE_BK_PLUS_QM    0x00000002
++#define RE_INTERVALS     0x00000200
++#define RE_LIMITED_OPS   0x00000400
++#define RE_NEWLINE_ALT   0x00000800
++#define RE_NO_BK_BRACES  0x00001000
++#define RE_NO_BK_PARENS  0x00002000
++#define RE_NO_BK_VBAR    0x00008000
++
++struct regex_quote_spec
++regex_quote_spec_gnu (unsigned long /*reg_syntax_t*/ syntax, bool anchored)
++{
++  struct regex_quote_spec result;
++  char *p;
++
++  p = result.special;
++  memcpy (p, bre_special, sizeof (bre_special) - 1);
++  p += sizeof (bre_special) - 1;
++  if ((syntax & RE_LIMITED_OPS) == 0 && (syntax & RE_BK_PLUS_QM) == 0)
++    {
++      *p++ = '+';
++      *p++ = '?';
++    }
++  if ((syntax & RE_INTERVALS) != 0 && (syntax & RE_NO_BK_BRACES) != 0)
++    {
++      *p++ = '{';
++      *p++ = '}';
++    }
++  if ((syntax & RE_NO_BK_PARENS) != 0)
++    {
++      *p++ = '(';
++      *p++ = ')';
++    }
++  if ((syntax & RE_LIMITED_OPS) == 0 && (syntax & RE_NO_BK_VBAR) != 0)
++    *p++ = '|';
++  if ((syntax & RE_NEWLINE_ALT) != 0)
++    *p++ = '\n';
++  *p = '\0';
++
++  result.multibyte = true;
++  result.anchored = anchored;
++
++  return result;
++}
++
++/* Characters that are special in a PCRE.  */
++static const char pcre_special[] = "$^.*[]\\+?{}()|";
++
++/* Options bit values, defined in <pcre.h>.  We don't include it here, because
++   it is not a standard header.  */
++#define PCRE_ANCHORED 0x00000010
++#define PCRE_EXTENDED 0x00000008
++
++struct regex_quote_spec
++regex_quote_spec_pcre (int options, bool anchored)
++{
++  struct regex_quote_spec result;
++  char *p;
++
++  p = result.special;
++  memcpy (p, bre_special, sizeof (pcre_special) - 1);
++  p += sizeof (pcre_special) - 1;
++  if (options & PCRE_EXTENDED)
++    {
++      *p++ = ' ';
++      *p++ = '\t';
++      *p++ = '\n';
++      *p++ = '\v';
++      *p++ = '\f';
++      *p++ = '\r';
++      *p++ = '#';
++    }
++  *p = '\0';
++
++  /* PCRE regular expressions consist of UTF-8 characters of options contains
++     PCRE_UTF8 and of single bytes otherwise.  */
++  result.multibyte = false;
++  /* If options contains PCRE_ANCHORED, the anchoring is implicit.  */
++  result.anchored = (options & PCRE_ANCHORED ? 0 : anchored);
++
++  return result;
++}
++
++size_t
++regex_quote_length (const char *string, const struct regex_quote_spec *spec)
++{
++  const char *special = spec->special;
++  size_t length;
++
++  length = 0;
++  if (spec->anchored)
++    length += 2; /* for '^' at the beginning and '$' at the end */
++  if (spec->multibyte)
++    {
++      mbui_iterator_t iter;
++
++      for (mbui_init (iter, string); mbui_avail (iter); mbui_advance (iter))
++        {
++          /* We know that special contains only ASCII characters.  */
++          if (mb_len (mbui_cur (iter)) == 1
++              && strchr (special, * mbui_cur_ptr (iter)))
++            length += 1;
++          length += mb_len (mbui_cur (iter));
++        }
++    }
++  else
++    {
++      const char *iter;
++
++      for (iter = string; *iter != '\0'; iter++)
++        {
++          if (strchr (special, *iter))
++            length += 1;
++          length += 1;
++        }
++    }
++
++  return length;
++}
++
++char *
++regex_quote_copy (char *p, const char *string, const struct regex_quote_spec *spec)
++{
++  const char *special = spec->special;
++
++  if (spec->anchored)
++    *p++ = '^';
++  if (spec->multibyte)
++    {
++      mbui_iterator_t iter;
++
++      for (mbui_init (iter, string); mbui_avail (iter); mbui_advance (iter))
++        {
++          /* We know that special contains only ASCII characters.  */
++          if (mb_len (mbui_cur (iter)) == 1
++              && strchr (special, * mbui_cur_ptr (iter)))
++            *p++ = '\\';
++          memcpy (p, mbui_cur_ptr (iter), mb_len (mbui_cur (iter)));
++          p += mb_len (mbui_cur (iter));
++        }
++    }
++  else
++    {
++      const char *iter;
++
++      for (iter = string; *iter != '\0'; iter++)
++        {
++          if (strchr (special, *iter))
++            *p++ = '\\';
++          *p++ = *iter++;
++        }
++    }
++  if (spec->anchored)
++    *p++ = '$';
++
++  return p;
++}
++
++char *
++regex_quote (const char *string, const struct regex_quote_spec *spec)
++{
++  size_t length = regex_quote_length (string, spec);
++  char *result = XNMALLOC (length + 1, char);
++  char *p;
++
++  p = result;
++  p = regex_quote_copy (p, string, spec);
++  *p = '\0';
++  return result;
++}
+--- origsrc/sed-4.2.2/lib/regex-quote.h	1970-01-01 01:00:00.000000000 +0100
++++ src/sed-4.2.2/lib/regex-quote.h	2013-06-27 18:05:27.112447751 +0200
+@@ -0,0 +1,88 @@
++/* Construct a regular expression from a literal string.
++   Copyright (C) 1995, 2010-2013 Free Software Foundation, Inc.
++   Written by Bruno Haible <haible@clisp.cons.org>, 2010.
++
++   This program is free software: you can redistribute it and/or modify
++   it under the terms of the GNU General Public License as published by
++   the Free Software Foundation; either version 3 of the License, or
++   (at your option) any later version.
++
++   This program is distributed in the hope that it will be useful,
++   but WITHOUT ANY WARRANTY; without even the implied warranty of
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
++   GNU General Public License for more details.
++
++   You should have received a copy of the GNU General Public License
++   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
++
++#ifndef _REGEX_QUOTE_H
++#define _REGEX_QUOTE_H
++
++#include <stddef.h>
++#include <stdbool.h>
++
++
++/* Specifies a quotation task for converting a fixed string to a regular
++   expression pattern.  */
++struct regex_quote_spec
++{
++  /* True if the regular expression pattern consists of multibyte characters
++     (in the encoding given by the LC_CTYPE category of the locale),
++     false if it consists of single bytes or UTF-8 characters.  */
++  unsigned int /*bool*/ multibyte : 1;
++  /* True if the regular expression pattern shall match only entire lines.  */
++  unsigned int /*bool*/ anchored : 1;
++  /* Set of characters that need to be escaped (all ASCII), as a
++     NUL-terminated string.  */
++  char special[30 + 1];
++};
++
++
++/* Creates a quotation task that produces a POSIX regular expression, that is,
++   a pattern that can be compiled with regcomp().
++   CFLAGS can be 0 or REG_EXTENDED.
++   If it is 0, the result is a Basic Regular Expression (BRE)
++   <http://www.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap09.html#tag_09_03>.
++   If it is REG_EXTENDED, the result is an Extended Regular Expression (ERE)
++   <http://www.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap09.html#tag_09_04>.
++   If ANCHORED is false, the regular expression will match substrings of lines.
++   If ANCHORED is true, it will match only complete lines,  */
++extern struct regex_quote_spec
++       regex_quote_spec_posix (int cflags, bool anchored);
++
++/* Creates a quotation task that produces a regular expression that can be
++   compiled with the GNU API function re_compile_pattern().
++   SYNTAX describes the syntax of the regular expression (such as
++   RE_SYNTAX_POSIX_BASIC, RE_SYNTAX_POSIX_EXTENDED, RE_SYNTAX_EMACS, all
++   defined in <regex.h>).  It must be the same value as 're_syntax_options'
++   at the moment of the re_compile_pattern() call.
++   If ANCHORED is false, the regular expression will match substrings of lines.
++   If ANCHORED is true, it will match only complete lines,  */
++extern struct regex_quote_spec
++       regex_quote_spec_gnu (unsigned long /*reg_syntax_t*/ syntax, bool anchored);
++
++/* Creates a quotation task that produces a PCRE regular expression, that is,
++   a pattern that can be compiled with pcre_compile().
++   OPTIONS is the same value as the second argument passed to pcre_compile().
++   If ANCHORED is false, the regular expression will match substrings of lines.
++   If ANCHORED is true, it will match only complete lines,  */
++extern struct regex_quote_spec
++       regex_quote_spec_pcre (int options, bool anchored);
++
++
++/* Returns the number of bytes needed for the quoted string.  */
++extern size_t
++       regex_quote_length (const char *string, const struct regex_quote_spec *spec);
++
++/* Copies the quoted string to p and returns the incremented p.
++   There must be room for regex_quote_length (string, spec) + 1 bytes at p.  */
++extern char *
++       regex_quote_copy (char *p,
++                         const char *string, const struct regex_quote_spec *spec);
++
++/* Returns the freshly allocated quoted string.  */
++extern char *
++       regex_quote (const char *string, const struct regex_quote_spec *spec);
++
++
++#endif /* _REGEX_QUOTE_H */
+--- origsrc/sed-4.2.2/lib/regex.c	2012-12-22 14:21:52.000000000 +0100
++++ src/sed-4.2.2/lib/regex.c	2013-06-27 18:05:27.138447639 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2003, 2005-2006, 2009-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ #ifndef _LIBC
+ # include <config.h>
+@@ -25,6 +24,7 @@
+ #  pragma GCC diagnostic ignored "-Wsuggest-attribute=pure"
+ # endif
+ # if (__GNUC__ == 4 && 3 <= __GNUC_MINOR__) || 4 < __GNUC__
++#  pragma GCC diagnostic ignored "-Wold-style-definition"
+ #  pragma GCC diagnostic ignored "-Wtype-limits"
+ # endif
+ #endif
+--- origsrc/sed-4.2.2/lib/regex.h	2012-12-22 14:21:52.000000000 +0100
++++ src/sed-4.2.2/lib/regex.h	2013-06-27 18:05:27.168447509 +0200
+@@ -1,23 +1,22 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Definitions for data structures and routines for the regular
+    expression library.
+-   Copyright (C) 1985, 1989-1993, 1995-1998, 2000-2003, 2005-2012
+-   Free Software Foundation, Inc.
++   Copyright (C) 1985, 1989-1993, 1995-1998, 2000-2003, 2005-2013 Free Software
++   Foundation, Inc.
+    This file is part of the GNU C Library.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ #ifndef _REGEX_H
+ #define _REGEX_H 1
+--- origsrc/sed-4.2.2/lib/regex_internal.c	2012-12-22 14:21:52.000000000 +0100
++++ src/sed-4.2.2/lib/regex_internal.c	2013-06-27 18:05:27.199447375 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ static void re_string_construct_common (const char *str, Idx len,
+ 					re_string_t *pstr,
+@@ -835,7 +834,7 @@ re_string_reconstruct (re_string_t *pstr
+ }
+ 
+ static unsigned char
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure))
+ re_string_peek_byte_case (const re_string_t *pstr, Idx idx)
+ {
+   int ch;
+@@ -975,7 +974,7 @@ re_node_set_alloc (re_node_set *set, Idx
+   set->alloc = size;
+   set->nelem = 0;
+   set->elems = re_malloc (Idx, size);
+-  if (BE (set->elems == NULL, 0))
++  if (BE (set->elems == NULL, 0) && (MALLOC_0_IS_NONNULL || size != 0))
+     return REG_ESPACE;
+   return REG_NOERROR;
+ }
+@@ -1355,7 +1354,7 @@ re_node_set_insert_last (re_node_set *se
+    Return true if SET1 and SET2 are equivalent.  */
+ 
+ static bool
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure))
+ re_node_set_compare (const re_node_set *set1, const re_node_set *set2)
+ {
+   Idx i;
+@@ -1370,7 +1369,7 @@ re_node_set_compare (const re_node_set *
+ /* Return (idx + 1) if SET contains the element ELEM, return 0 otherwise.  */
+ 
+ static Idx
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure))
+ re_node_set_contains (const re_node_set *set, Idx elem)
+ {
+   __re_size_t idx, right, mid;
+@@ -1444,11 +1443,9 @@ re_dfa_add_node (re_dfa_t *dfa, re_token
+   dfa->nodes[dfa->nodes_len] = token;
+   dfa->nodes[dfa->nodes_len].constraint = 0;
+ #ifdef RE_ENABLE_I18N
+-  {
+-  int type = token.type;
+   dfa->nodes[dfa->nodes_len].accept_mb =
+-    (type == OP_PERIOD && dfa->mb_cur_max > 1) || type == COMPLEX_BRACKET;
+-  }
++    ((token.type == OP_PERIOD && dfa->mb_cur_max > 1)
++     || token.type == COMPLEX_BRACKET);
+ #endif
+   dfa->nexts[dfa->nodes_len] = REG_MISSING;
+   re_node_set_init_empty (dfa->edests + dfa->nodes_len);
+--- origsrc/sed-4.2.2/lib/regex_internal.h	2012-12-22 14:21:52.000000000 +0100
++++ src/sed-4.2.2/lib/regex_internal.h	2013-06-27 18:05:27.230447242 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ #ifndef _REGEX_INTERNAL_H
+ #define _REGEX_INTERNAL_H 1
+@@ -28,21 +27,54 @@
+ #include <string.h>
+ 
+ #include <langinfo.h>
+-#ifndef _LIBC
+-# include "localcharset.h"
+-#endif
+ #include <locale.h>
+ #include <wchar.h>
+ #include <wctype.h>
+ #include <stdbool.h>
+ #include <stdint.h>
+-#if defined _LIBC
++
++#ifdef _LIBC
+ # include <bits/libc-lock.h>
++# define lock_define(name) __libc_lock_define (, name)
++# define lock_init(lock) (__libc_lock_init (lock), 0)
++# define lock_fini(lock) 0
++# define lock_lock(lock) __libc_lock_lock (lock)
++# define lock_unlock(lock) __libc_lock_unlock (lock)
++#elif defined GNULIB_LOCK
++# include "glthread/lock.h"
++  /* Use gl_lock_define if empty macro arguments are known to work.
++     Otherwise, fall back on less-portable substitutes.  */
++# if ((defined __GNUC__ && !defined __STRICT_ANSI__) \
++      || (defined __STDC_VERSION__ && 199901L <= __STDC_VERSION__))
++#  define lock_define(name) gl_lock_define (, name)
++# elif USE_POSIX_THREADS
++#  define lock_define(name) pthread_mutex_t name;
++# elif USE_PTH_THREADS
++#  define lock_define(name) pth_mutex_t name;
++# elif USE_SOLARIS_THREADS
++#  define lock_define(name) mutex_t name;
++# elif USE_WINDOWS_THREADS
++#  define lock_define(name) gl_lock_t name;
++# else
++#  define lock_define(name)
++# endif
++# define lock_init(lock) glthread_lock_init (&(lock))
++# define lock_fini(lock) glthread_lock_destroy (&(lock))
++# define lock_lock(lock) glthread_lock_lock (&(lock))
++# define lock_unlock(lock) glthread_lock_unlock (&(lock))
++#elif defined GNULIB_PTHREAD
++# include <pthread.h>
++# define lock_define(name) pthread_mutex_t name;
++# define lock_init(lock) pthread_mutex_init (&(lock), 0)
++# define lock_fini(lock) pthread_mutex_destroy (&(lock))
++# define lock_lock(lock) pthread_mutex_lock (&(lock))
++# define lock_unlock(lock) pthread_mutex_unlock (&(lock))
+ #else
+-# define __libc_lock_define(CLASS,NAME)
+-# define __libc_lock_init(NAME) do { } while (0)
+-# define __libc_lock_lock(NAME) do { } while (0)
+-# define __libc_lock_unlock(NAME) do { } while (0)
++# define lock_define(name)
++# define lock_init(lock) 0
++# define lock_fini(lock) 0
++# define lock_lock(lock) ((void) 0)
++# define lock_unlock(lock) ((void) 0)
+ #endif
+ 
+ /* In case that the system doesn't have isblank().  */
+@@ -65,7 +97,7 @@
+ # ifdef _LIBC
+ #  undef gettext
+ #  define gettext(msgid) \
+-  INTUSE(__dcgettext) (_libc_intl_domainname, msgid, LC_MESSAGES)
++  __dcgettext (_libc_intl_domainname, msgid, LC_MESSAGES)
+ # endif
+ #else
+ # define gettext(msgid) (msgid)
+@@ -101,6 +133,8 @@
+ 
+ /* Rename to standard API for using out of glibc.  */
+ #ifndef _LIBC
++# undef __wctype
++# undef __iswctype
+ # define __wctype wctype
+ # define __iswctype iswctype
+ # define __btowc btowc
+@@ -110,10 +144,8 @@
+ # define attribute_hidden
+ #endif /* not _LIBC */
+ 
+-#if __GNUC__ >= 4 || (__GNUC__ == 3 && __GNUC_MINOR__ >= 1)
+-# define __attribute(arg) __attribute__ (arg)
+-#else
+-# define __attribute(arg)
++#if __GNUC__ < 3 + (__GNUC_MINOR__ < 1)
++# define __attribute__(arg)
+ #endif
+ 
+ typedef __re_idx_t Idx;
+@@ -429,7 +461,7 @@ static void build_upper_buffer (re_strin
+ static void re_string_translate_buffer (re_string_t *pstr) internal_function;
+ static unsigned int re_string_context_at (const re_string_t *input, Idx idx,
+ 					  int eflags)
+-     internal_function __attribute ((pure));
++     internal_function __attribute__ ((pure));
+ #endif
+ #define re_string_peek_byte(pstr, offset) \
+   ((pstr)->mbs[(pstr)->cur_idx + offset])
+@@ -448,7 +480,9 @@ static unsigned int re_string_context_at
+ #define re_string_skip_bytes(pstr,idx) ((pstr)->cur_idx += (idx))
+ #define re_string_set_index(pstr,idx) ((pstr)->cur_idx = (idx))
+ 
+-#include <alloca.h>
++#if defined _LIBC || HAVE_ALLOCA
++# include <alloca.h>
++#endif
+ 
+ #ifndef _LIBC
+ # if HAVE_ALLOCA
+@@ -465,6 +499,12 @@ static unsigned int re_string_context_at
+ # endif
+ #endif
+ 
++#ifdef _LIBC
++# define MALLOC_0_IS_NONNULL 1
++#elif !defined MALLOC_0_IS_NONNULL
++# define MALLOC_0_IS_NONNULL 0
++#endif
++
+ #ifndef MAX
+ # define MAX(a,b) ((a) < (b) ? (b) : (a))
+ #endif
+@@ -695,7 +735,7 @@ struct re_dfa_t
+ #ifdef DEBUG
+   char* re_str;
+ #endif
+-  __libc_lock_define (, lock)
++  lock_define (lock)
+ };
+ 
+ #define re_node_set_init_empty(set) memset (set, '\0', sizeof (re_node_set))
+@@ -767,7 +807,7 @@ bitset_copy (bitset_t dest, const bitset
+   memcpy (dest, src, sizeof (bitset_t));
+ }
+ 
+-static void
++static void __attribute__ ((unused))
+ bitset_not (bitset_t set)
+ {
+   int bitset_i;
+@@ -779,7 +819,7 @@ bitset_not (bitset_t set)
+        & ~set[BITSET_WORDS - 1]);
+ }
+ 
+-static void
++static void __attribute__ ((unused))
+ bitset_merge (bitset_t dest, const bitset_t src)
+ {
+   int bitset_i;
+@@ -787,7 +827,7 @@ bitset_merge (bitset_t dest, const bitse
+     dest[bitset_i] |= src[bitset_i];
+ }
+ 
+-static void
++static void __attribute__ ((unused))
+ bitset_mask (bitset_t dest, const bitset_t src)
+ {
+   int bitset_i;
+@@ -798,7 +838,7 @@ bitset_mask (bitset_t dest, const bitset
+ #ifdef RE_ENABLE_I18N
+ /* Functions for re_string.  */
+ static int
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure, unused))
+ re_string_char_size_at (const re_string_t *pstr, Idx idx)
+ {
+   int byte_idx;
+@@ -811,7 +851,7 @@ re_string_char_size_at (const re_string_
+ }
+ 
+ static wint_t
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure, unused))
+ re_string_wchar_at (const re_string_t *pstr, Idx idx)
+ {
+   if (pstr->mb_cur_max == 1)
+@@ -821,7 +861,7 @@ re_string_wchar_at (const re_string_t *p
+ 
+ # ifndef NOT_IN_libc
+ static int
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure, unused))
+ re_string_elem_size_at (const re_string_t *pstr, Idx idx)
+ {
+ #  ifdef _LIBC
+--- origsrc/sed-4.2.2/lib/regexec.c	2012-12-22 14:21:52.000000000 +0100
++++ src/sed-4.2.2/lib/regexec.c	2013-06-27 18:05:27.268447078 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ static reg_errcode_t match_ctx_init (re_match_context_t *cache, int eflags,
+ 				     Idx n) internal_function;
+@@ -200,7 +199,7 @@ static Idx group_nodes_into_DFAstates (c
+ static bool check_node_accept (const re_match_context_t *mctx,
+ 			       const re_token_t *node, Idx idx)
+      internal_function;
+-static reg_errcode_t extend_buffers (re_match_context_t *mctx)
++static reg_errcode_t extend_buffers (re_match_context_t *mctx, int min_len)
+      internal_function;
+ 
+ /* Entry point for POSIX code.  */
+@@ -229,9 +228,7 @@ regexec (preg, string, nmatch, pmatch, e
+ {
+   reg_errcode_t err;
+   Idx start, length;
+-#ifdef _LIBC
+   re_dfa_t *dfa = preg->buffer;
+-#endif
+ 
+   if (eflags & ~(REG_NOTBOL | REG_NOTEOL | REG_STARTEND))
+     return REG_BADPAT;
+@@ -247,14 +244,14 @@ regexec (preg, string, nmatch, pmatch, e
+       length = strlen (string);
+     }
+ 
+-  __libc_lock_lock (dfa->lock);
++  lock_lock (dfa->lock);
+   if (preg->no_sub)
+     err = re_search_internal (preg, string, length, start, length,
+ 			      length, 0, NULL, eflags);
+   else
+     err = re_search_internal (preg, string, length, start, length,
+ 			      length, nmatch, pmatch, eflags);
+-  __libc_lock_unlock (dfa->lock);
++  lock_unlock (dfa->lock);
+   return err != REG_NOERROR;
+ }
+ 
+@@ -422,9 +419,7 @@ re_search_stub (struct re_pattern_buffer
+   Idx nregs;
+   regoff_t rval;
+   int eflags = 0;
+-#ifdef _LIBC
+   re_dfa_t *dfa = bufp->buffer;
+-#endif
+   Idx last_start = start + range;
+ 
+   /* Check for out-of-range.  */
+@@ -435,7 +430,7 @@ re_search_stub (struct re_pattern_buffer
+   else if (BE (last_start < 0 || (range < 0 && start <= last_start), 0))
+     last_start = 0;
+ 
+-  __libc_lock_lock (dfa->lock);
++  lock_lock (dfa->lock);
+ 
+   eflags |= (bufp->not_bol) ? REG_NOTBOL : 0;
+   eflags |= (bufp->not_eol) ? REG_NOTEOL : 0;
+@@ -499,7 +494,7 @@ re_search_stub (struct re_pattern_buffer
+     }
+   re_free (pmatch);
+  out:
+-  __libc_lock_unlock (dfa->lock);
++  lock_unlock (dfa->lock);
+   return rval;
+ }
+ 
+@@ -1065,7 +1060,7 @@ prune_impossible_nodes (re_match_context
+    since initial states may have constraints like "\<", "^", etc..  */
+ 
+ static inline re_dfastate_t *
+-__attribute ((always_inline)) internal_function
++__attribute__ ((always_inline)) internal_function
+ acquire_init_state_context (reg_errcode_t *err, const re_match_context_t *mctx,
+ 			    Idx idx)
+ {
+@@ -1177,7 +1172,7 @@ check_matching (re_match_context_t *mctx
+ 	  || (BE (next_char_idx >= mctx->input.valid_len, 0)
+ 	      && mctx->input.valid_len < mctx->input.len))
+ 	{
+-	  err = extend_buffers (mctx);
++	  err = extend_buffers (mctx, next_char_idx + 1);
+ 	  if (BE (err != REG_NOERROR, 0))
+ 	    {
+ 	      assert (err == REG_ESPACE);
+@@ -1757,7 +1752,7 @@ clean_state_log_if_needed (re_match_cont
+ 	  && mctx->input.valid_len < mctx->input.len))
+     {
+       reg_errcode_t err;
+-      err = extend_buffers (mctx);
++      err = extend_buffers (mctx, next_state_log_idx + 1);
+       if (BE (err != REG_NOERROR, 0))
+ 	return err;
+     }
+@@ -2814,7 +2809,7 @@ get_subexp (re_match_context_t *mctx, Id
+ 		  if (bkref_str_off >= mctx->input.len)
+ 		    break;
+ 
+-		  err = extend_buffers (mctx);
++		  err = extend_buffers (mctx, bkref_str_off + 1);
+ 		  if (BE (err != REG_NOERROR, 0))
+ 		    return err;
+ 
+@@ -3937,6 +3932,7 @@ check_node_accept_bytes (const re_dfa_t
+ 		in_collseq = find_collation_sequence_value (pin, elem_len);
+ 	    }
+ 	  /* match with range expression?  */
++	  /* FIXME: Implement rational ranges here, too.  */
+ 	  for (i = 0; i < cset->nranges; ++i)
+ 	    if (cset->range_starts[i] <= in_collseq
+ 		&& in_collseq <= cset->range_ends[i])
+@@ -3988,18 +3984,9 @@ check_node_accept_bytes (const re_dfa_t
+ # endif /* _LIBC */
+ 	{
+ 	  /* match with range expression?  */
+-#if __GNUC__ >= 2 && ! (__STDC_VERSION__ < 199901L && defined __STRICT_ANSI__)
+-	  wchar_t cmp_buf[] = {L'\0', L'\0', wc, L'\0', L'\0', L'\0'};
+-#else
+-	  wchar_t cmp_buf[] = {L'\0', L'\0', L'\0', L'\0', L'\0', L'\0'};
+-	  cmp_buf[2] = wc;
+-#endif
+ 	  for (i = 0; i < cset->nranges; ++i)
+ 	    {
+-	      cmp_buf[0] = cset->range_starts[i];
+-	      cmp_buf[4] = cset->range_ends[i];
+-	      if (wcscoll (cmp_buf, cmp_buf + 2) <= 0
+-		  && wcscoll (cmp_buf + 2, cmp_buf + 4) <= 0)
++	      if (cset->range_starts[i] <= wc && wc <= cset->range_ends[i])
+ 		{
+ 		  match_len = char_len;
+ 		  goto check_node_accept_bytes_match;
+@@ -4137,7 +4124,7 @@ check_node_accept (const re_match_contex
+ 
+ static reg_errcode_t
+ internal_function __attribute_warn_unused_result__
+-extend_buffers (re_match_context_t *mctx)
++extend_buffers (re_match_context_t *mctx, int min_len)
+ {
+   reg_errcode_t ret;
+   re_string_t *pstr = &mctx->input;
+@@ -4147,8 +4134,10 @@ extend_buffers (re_match_context_t *mctx
+           <= pstr->bufs_len, 0))
+     return REG_ESPACE;
+ 
+-  /* Double the lengths of the buffers.  */
+-  ret = re_string_realloc_buffers (pstr, MIN (pstr->len, pstr->bufs_len * 2));
++  /* Double the lengths of the buffers, but allocate at least MIN_LEN.  */
++  ret = re_string_realloc_buffers (pstr,
++				   MAX (min_len,
++					MIN (pstr->len, pstr->bufs_len * 2)));
+   if (BE (ret != REG_NOERROR, 0))
+     return ret;
+ 
+--- origsrc/sed-4.2.2/sed/sed.c	2012-03-16 10:13:31.000000000 +0100
++++ src/sed-4.2.2/sed/sed.c	2013-06-27 18:06:25.592195456 +0200
+@@ -57,7 +57,11 @@ bool follow_symlinks = false;
+ char *in_place_extension = NULL;
+ 
+ /* The mode to use to read/write files, either "r"/"w" or "rb"/"wb".  */
++#ifdef HAVE_FOPEN_RT
++char *read_mode = "rt";
++#else
+ char *read_mode = "r";
++#endif
+ char *write_mode = "w";
+ 
+ /* Do we need to be pedantically POSIX compliant? */
diff --git a/dev/build/windows/patches_coq/sed-4.2.2.patch b/dev/build/windows/patches_coq/sed-4.2.2.patch
new file mode 100755
index 000000000..c7ccd53c7
--- /dev/null
+++ b/dev/build/windows/patches_coq/sed-4.2.2.patch
@@ -0,0 +1,1301 @@
+--- origsrc/doc/sed.1	2012-12-22 15:27:13.000000000 +0100
++++ src/doc/sed.1	2013-06-27 18:10:47.974060492 +0200
+@@ -1,5 +1,5 @@
+ .\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.28.
+-.TH SED "1" "December 2012" "sed 4.2.2" "User Commands"
++.TH SED "1" "June 2013" "sed 4.2.2" "User Commands"
+ .SH NAME
+ sed \- stream editor for filtering and transforming text
+ .SH SYNOPSIS
+@@ -40,6 +40,10 @@ follow symlinks when processing in place
+ .IP
+ edit files in place (makes backup if SUFFIX supplied)
+ .HP
++\fB\-b\fR, \fB\-\-binary\fR
++.IP
++open files in binary mode (CR+LFs are not processed specially)
++.HP
+ \fB\-l\fR N, \fB\-\-line\-length\fR=\fIN\fR
+ .IP
+ specify the desired line-wrap length for the `l' command
+--- origsrc/lib/regcomp.c	2012-12-22 14:21:52.000000000 +0100
++++ src/lib/regcomp.c	2013-06-27 18:05:27.044448044 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ static reg_errcode_t re_compile_internal (regex_t *preg, const char * pattern,
+ 					  size_t length, reg_syntax_t syntax);
+@@ -95,20 +94,20 @@ static reg_errcode_t build_charclass (RE
+ 				      bitset_t sbcset,
+ 				      re_charset_t *mbcset,
+ 				      Idx *char_class_alloc,
+-				      const unsigned char *class_name,
++				      const char *class_name,
+ 				      reg_syntax_t syntax);
+ #else  /* not RE_ENABLE_I18N */
+ static reg_errcode_t build_equiv_class (bitset_t sbcset,
+ 					const unsigned char *name);
+ static reg_errcode_t build_charclass (RE_TRANSLATE_TYPE trans,
+ 				      bitset_t sbcset,
+-				      const unsigned char *class_name,
++				      const char *class_name,
+ 				      reg_syntax_t syntax);
+ #endif /* not RE_ENABLE_I18N */
+ static bin_tree_t *build_charclass_op (re_dfa_t *dfa,
+ 				       RE_TRANSLATE_TYPE trans,
+-				       const unsigned char *class_name,
+-				       const unsigned char *extra,
++				       const char *class_name,
++				       const char *extra,
+ 				       bool non_match, reg_errcode_t *err);
+ static bin_tree_t *create_tree (re_dfa_t *dfa,
+ 				bin_tree_t *left, bin_tree_t *right,
+@@ -293,7 +292,7 @@ weak_alias (__re_compile_fastmap, re_com
+ #endif
+ 
+ static inline void
+-__attribute ((always_inline))
++__attribute__ ((always_inline))
+ re_set_fastmap (char *fastmap, bool icase, int ch)
+ {
+   fastmap[ch] = 1;
+@@ -587,7 +586,7 @@ weak_alias (__regerror, regerror)
+ static const bitset_t utf8_sb_map =
+ {
+   /* Set the first 128 bits.  */
+-# ifdef __GNUC__
++# if defined __GNUC__ && !defined __STRICT_ANSI__
+   [0 ... 0x80 / BITSET_WORD_BITS - 1] = BITSET_WORD_MAX
+ # else
+ #  if 4 * BITSET_WORD_BITS < ASCII_CHARS
+@@ -664,7 +663,10 @@ regfree (preg)
+ {
+   re_dfa_t *dfa = preg->buffer;
+   if (BE (dfa != NULL, 1))
+-    free_dfa_content (dfa);
++    {
++      lock_fini (dfa->lock);
++      free_dfa_content (dfa);
++    }
+   preg->buffer = NULL;
+   preg->allocated = 0;
+ 
+@@ -785,6 +787,8 @@ re_compile_internal (regex_t *preg, cons
+   preg->used = sizeof (re_dfa_t);
+ 
+   err = init_dfa (dfa, length);
++  if (BE (err == REG_NOERROR && lock_init (dfa->lock) != 0, 0))
++    err = REG_ESPACE;
+   if (BE (err != REG_NOERROR, 0))
+     {
+       free_dfa_content (dfa);
+@@ -798,8 +802,6 @@ re_compile_internal (regex_t *preg, cons
+   strncpy (dfa->re_str, pattern, length + 1);
+ #endif
+ 
+-  __libc_lock_init (dfa->lock);
+-
+   err = re_string_construct (&regexp, pattern, length, preg->translate,
+ 			     (syntax & RE_ICASE) != 0, dfa);
+   if (BE (err != REG_NOERROR, 0))
+@@ -807,6 +809,7 @@ re_compile_internal (regex_t *preg, cons
+     re_compile_internal_free_return:
+       free_workarea_compile (preg);
+       re_string_destruct (&regexp);
++      lock_fini (dfa->lock);
+       free_dfa_content (dfa);
+       preg->buffer = NULL;
+       preg->allocated = 0;
+@@ -839,6 +842,7 @@ re_compile_internal (regex_t *preg, cons
+ 
+   if (BE (err != REG_NOERROR, 0))
+     {
++      lock_fini (dfa->lock);
+       free_dfa_content (dfa);
+       preg->buffer = NULL;
+       preg->allocated = 0;
+@@ -954,10 +958,10 @@ static void
+ internal_function
+ init_word_char (re_dfa_t *dfa)
+ {
+-  dfa->word_ops_used = 1;
+   int i = 0;
+   int j;
+   int ch = 0;
++  dfa->word_ops_used = 1;
+   if (BE (dfa->map_notascii == 0, 1))
+     {
+       bitset_word_t bits0 = 0x00000000;
+@@ -2423,8 +2427,8 @@ parse_expression (re_string_t *regexp, r
+     case OP_WORD:
+     case OP_NOTWORD:
+       tree = build_charclass_op (dfa, regexp->trans,
+-				 (const unsigned char *) "alnum",
+-				 (const unsigned char *) "_",
++				 "alnum",
++				 "_",
+ 				 token->type == OP_NOTWORD, err);
+       if (BE (*err != REG_NOERROR && tree == NULL, 0))
+ 	return NULL;
+@@ -2432,8 +2436,8 @@ parse_expression (re_string_t *regexp, r
+     case OP_SPACE:
+     case OP_NOTSPACE:
+       tree = build_charclass_op (dfa, regexp->trans,
+-				 (const unsigned char *) "space",
+-				 (const unsigned char *) "",
++				 "space",
++				 "",
+ 				 token->type == OP_NOTSPACE, err);
+       if (BE (*err != REG_NOERROR && tree == NULL, 0))
+ 	return NULL;
+@@ -2713,7 +2717,6 @@ build_range_exp (const reg_syntax_t synt
+     wchar_t wc;
+     wint_t start_wc;
+     wint_t end_wc;
+-    wchar_t cmp_buf[6] = {L'\0', L'\0', L'\0', L'\0', L'\0', L'\0'};
+ 
+     start_ch = ((start_elem->type == SB_CHAR) ? start_elem->opr.ch
+ 		: ((start_elem->type == COLL_SYM) ? start_elem->opr.name[0]
+@@ -2727,11 +2730,7 @@ build_range_exp (const reg_syntax_t synt
+ 	      ? __btowc (end_ch) : end_elem->opr.wch);
+     if (start_wc == WEOF || end_wc == WEOF)
+       return REG_ECOLLATE;
+-    cmp_buf[0] = start_wc;
+-    cmp_buf[4] = end_wc;
+-
+-    if (BE ((syntax & RE_NO_EMPTY_RANGES)
+-            && wcscoll (cmp_buf, cmp_buf + 4) > 0, 0))
++    else if (BE ((syntax & RE_NO_EMPTY_RANGES) && start_wc > end_wc, 0))
+       return REG_ERANGE;
+ 
+     /* Got valid collation sequence values, add them as a new entry.
+@@ -2772,9 +2771,7 @@ build_range_exp (const reg_syntax_t synt
+     /* Build the table for single byte characters.  */
+     for (wc = 0; wc < SBC_MAX; ++wc)
+       {
+-	cmp_buf[2] = wc;
+-	if (wcscoll (cmp_buf, cmp_buf + 2) <= 0
+-	    && wcscoll (cmp_buf + 2, cmp_buf + 4) <= 0)
++	if (start_wc <= wc && wc <= end_wc)
+ 	  bitset_set (sbcset, wc);
+       }
+   }
+@@ -2843,40 +2840,29 @@ parse_bracket_exp (re_string_t *regexp,
+ 
+   /* Local function for parse_bracket_exp used in _LIBC environment.
+      Seek the collating symbol entry corresponding to NAME.
+-     Return the index of the symbol in the SYMB_TABLE.  */
++     Return the index of the symbol in the SYMB_TABLE,
++     or -1 if not found.  */
+ 
+   auto inline int32_t
+-  __attribute ((always_inline))
+-  seek_collating_symbol_entry (name, name_len)
+-	 const unsigned char *name;
+-	 size_t name_len;
+-    {
+-      int32_t hash = elem_hash ((const char *) name, name_len);
+-      int32_t elem = hash % table_size;
+-      if (symb_table[2 * elem] != 0)
+-	{
+-	  int32_t second = hash % (table_size - 2) + 1;
+-
+-	  do
+-	    {
+-	      /* First compare the hashing value.  */
+-	      if (symb_table[2 * elem] == hash
+-		  /* Compare the length of the name.  */
+-		  && name_len == extra[symb_table[2 * elem + 1]]
+-		  /* Compare the name.  */
+-		  && memcmp (name, &extra[symb_table[2 * elem + 1] + 1],
+-			     name_len) == 0)
+-		{
+-		  /* Yep, this is the entry.  */
+-		  break;
+-		}
++  __attribute__ ((always_inline))
++  seek_collating_symbol_entry (const unsigned char *name, size_t name_len)
++    {
++      int32_t elem;
+ 
+-	      /* Next entry.  */
+-	      elem += second;
+-	    }
+-	  while (symb_table[2 * elem] != 0);
+-	}
+-      return elem;
++      for (elem = 0; elem < table_size; elem++)
++	if (symb_table[2 * elem] != 0)
++	  {
++	    int32_t idx = symb_table[2 * elem + 1];
++	    /* Skip the name of collating element name.  */
++	    idx += 1 + extra[idx];
++	    if (/* Compare the length of the name.  */
++		name_len == extra[idx]
++		/* Compare the name.  */
++		&& memcmp (name, &extra[idx + 1], name_len) == 0)
++	      /* Yep, this is the entry.  */
++	      return elem;
++	  }
++      return -1;
+     }
+ 
+   /* Local function for parse_bracket_exp used in _LIBC environment.
+@@ -2884,9 +2870,8 @@ parse_bracket_exp (re_string_t *regexp,
+      Return the value if succeeded, UINT_MAX otherwise.  */
+ 
+   auto inline unsigned int
+-  __attribute ((always_inline))
+-  lookup_collation_sequence_value (br_elem)
+-	 bracket_elem_t *br_elem;
++  __attribute__ ((always_inline))
++  lookup_collation_sequence_value (bracket_elem_t *br_elem)
+     {
+       if (br_elem->type == SB_CHAR)
+ 	{
+@@ -2914,7 +2899,7 @@ parse_bracket_exp (re_string_t *regexp,
+ 	      int32_t elem, idx;
+ 	      elem = seek_collating_symbol_entry (br_elem->opr.name,
+ 						  sym_name_len);
+-	      if (symb_table[2 * elem] != 0)
++	      if (elem != -1)
+ 		{
+ 		  /* We found the entry.  */
+ 		  idx = symb_table[2 * elem + 1];
+@@ -2932,7 +2917,7 @@ parse_bracket_exp (re_string_t *regexp,
+ 		  /* Return the collation sequence value.  */
+ 		  return *(unsigned int *) (extra + idx);
+ 		}
+-	      else if (symb_table[2 * elem] == 0 && sym_name_len == 1)
++	      else if (sym_name_len == 1)
+ 		{
+ 		  /* No valid character.  Match it as a single byte
+ 		     character.  */
+@@ -2953,12 +2938,9 @@ parse_bracket_exp (re_string_t *regexp,
+      update it.  */
+ 
+   auto inline reg_errcode_t
+-  __attribute ((always_inline))
+-  build_range_exp (sbcset, mbcset, range_alloc, start_elem, end_elem)
+-	 re_charset_t *mbcset;
+-	 Idx *range_alloc;
+-	 bitset_t sbcset;
+-	 bracket_elem_t *start_elem, *end_elem;
++  __attribute__ ((always_inline))
++  build_range_exp (bitset_t sbcset, re_charset_t *mbcset, int *range_alloc,
++		   bracket_elem_t *start_elem, bracket_elem_t *end_elem)
+     {
+       unsigned int ch;
+       uint32_t start_collseq;
+@@ -2971,6 +2953,7 @@ parse_bracket_exp (re_string_t *regexp,
+ 	      0))
+ 	return REG_ERANGE;
+ 
++      /* FIXME: Implement rational ranges here, too.  */
+       start_collseq = lookup_collation_sequence_value (start_elem);
+       end_collseq = lookup_collation_sequence_value (end_elem);
+       /* Check start/end collation sequence values.  */
+@@ -3036,26 +3019,23 @@ parse_bracket_exp (re_string_t *regexp,
+      pointer argument since we may update it.  */
+ 
+   auto inline reg_errcode_t
+-  __attribute ((always_inline))
+-  build_collating_symbol (sbcset, mbcset, coll_sym_alloc, name)
+-	 re_charset_t *mbcset;
+-	 Idx *coll_sym_alloc;
+-	 bitset_t sbcset;
+-	 const unsigned char *name;
++  __attribute__ ((always_inline))
++  build_collating_symbol (bitset_t sbcset, re_charset_t *mbcset,
++			  Idx *coll_sym_alloc, const unsigned char *name)
+     {
+       int32_t elem, idx;
+       size_t name_len = strlen ((const char *) name);
+       if (nrules != 0)
+ 	{
+ 	  elem = seek_collating_symbol_entry (name, name_len);
+-	  if (symb_table[2 * elem] != 0)
++	  if (elem != -1)
+ 	    {
+ 	      /* We found the entry.  */
+ 	      idx = symb_table[2 * elem + 1];
+ 	      /* Skip the name of collating element name.  */
+ 	      idx += 1 + extra[idx];
+ 	    }
+-	  else if (symb_table[2 * elem] == 0 && name_len == 1)
++	  else if (name_len == 1)
+ 	    {
+ 	      /* No valid character, treat it as a normal
+ 		 character.  */
+@@ -3298,7 +3278,8 @@ parse_bracket_exp (re_string_t *regexp,
+ #ifdef RE_ENABLE_I18N
+ 				      mbcset, &char_class_alloc,
+ #endif /* RE_ENABLE_I18N */
+-				      start_elem.opr.name, syntax);
++				      (const char *) start_elem.opr.name,
++				      syntax);
+ 	      if (BE (*err != REG_NOERROR, 0))
+ 	       goto parse_bracket_exp_free_return;
+ 	      break;
+@@ -3578,14 +3559,14 @@ static reg_errcode_t
+ #ifdef RE_ENABLE_I18N
+ build_charclass (RE_TRANSLATE_TYPE trans, bitset_t sbcset,
+ 		 re_charset_t *mbcset, Idx *char_class_alloc,
+-		 const unsigned char *class_name, reg_syntax_t syntax)
++		 const char *class_name, reg_syntax_t syntax)
+ #else /* not RE_ENABLE_I18N */
+ build_charclass (RE_TRANSLATE_TYPE trans, bitset_t sbcset,
+-		 const unsigned char *class_name, reg_syntax_t syntax)
++		 const char *class_name, reg_syntax_t syntax)
+ #endif /* not RE_ENABLE_I18N */
+ {
+   int i;
+-  const char *name = (const char *) class_name;
++  const char *name = class_name;
+ 
+   /* In case of REG_ICASE "upper" and "lower" match the both of
+      upper and lower cases.  */
+@@ -3659,8 +3640,8 @@ build_charclass (RE_TRANSLATE_TYPE trans
+ 
+ static bin_tree_t *
+ build_charclass_op (re_dfa_t *dfa, RE_TRANSLATE_TYPE trans,
+-		    const unsigned char *class_name,
+-		    const unsigned char *extra, bool non_match,
++		    const char *class_name,
++		    const char *extra, bool non_match,
+ 		    reg_errcode_t *err)
+ {
+   re_bitset_ptr_t sbcset;
+--- origsrc/lib/regex-quote.c	1970-01-01 01:00:00.000000000 +0100
++++ src/lib/regex-quote.c	2013-06-27 18:05:27.081447884 +0200
+@@ -0,0 +1,216 @@
++/* Construct a regular expression from a literal string.
++   Copyright (C) 1995, 2010-2013 Free Software Foundation, Inc.
++   Written by Bruno Haible <haible@clisp.cons.org>, 2010.
++
++   This program is free software: you can redistribute it and/or modify
++   it under the terms of the GNU General Public License as published by
++   the Free Software Foundation; either version 3 of the License, or
++   (at your option) any later version.
++
++   This program is distributed in the hope that it will be useful,
++   but WITHOUT ANY WARRANTY; without even the implied warranty of
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
++   GNU General Public License for more details.
++
++   You should have received a copy of the GNU General Public License
++   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
++
++#include <config.h>
++
++/* Specification.  */
++#include "regex-quote.h"
++
++#include <string.h>
++
++#include "mbuiter.h"
++#include "xalloc.h"
++
++/* Characters that are special in a BRE.  */
++static const char bre_special[] = "$^.*[]\\";
++
++/* Characters that are special in an ERE.  */
++static const char ere_special[] = "$^.*[]\\+?{}()|";
++
++struct regex_quote_spec
++regex_quote_spec_posix (int cflags, bool anchored)
++{
++  struct regex_quote_spec result;
++
++  strcpy (result.special, cflags != 0 ? ere_special : bre_special);
++  result.multibyte = true;
++  result.anchored = anchored;
++
++  return result;
++}
++
++/* Syntax bit values, defined in GNU <regex.h>.  We don't include it here,
++   otherwise this module would need to depend on gnulib module 'regex'.  */
++#define RE_BK_PLUS_QM    0x00000002
++#define RE_INTERVALS     0x00000200
++#define RE_LIMITED_OPS   0x00000400
++#define RE_NEWLINE_ALT   0x00000800
++#define RE_NO_BK_BRACES  0x00001000
++#define RE_NO_BK_PARENS  0x00002000
++#define RE_NO_BK_VBAR    0x00008000
++
++struct regex_quote_spec
++regex_quote_spec_gnu (unsigned long /*reg_syntax_t*/ syntax, bool anchored)
++{
++  struct regex_quote_spec result;
++  char *p;
++
++  p = result.special;
++  memcpy (p, bre_special, sizeof (bre_special) - 1);
++  p += sizeof (bre_special) - 1;
++  if ((syntax & RE_LIMITED_OPS) == 0 && (syntax & RE_BK_PLUS_QM) == 0)
++    {
++      *p++ = '+';
++      *p++ = '?';
++    }
++  if ((syntax & RE_INTERVALS) != 0 && (syntax & RE_NO_BK_BRACES) != 0)
++    {
++      *p++ = '{';
++      *p++ = '}';
++    }
++  if ((syntax & RE_NO_BK_PARENS) != 0)
++    {
++      *p++ = '(';
++      *p++ = ')';
++    }
++  if ((syntax & RE_LIMITED_OPS) == 0 && (syntax & RE_NO_BK_VBAR) != 0)
++    *p++ = '|';
++  if ((syntax & RE_NEWLINE_ALT) != 0)
++    *p++ = '\n';
++  *p = '\0';
++
++  result.multibyte = true;
++  result.anchored = anchored;
++
++  return result;
++}
++
++/* Characters that are special in a PCRE.  */
++static const char pcre_special[] = "$^.*[]\\+?{}()|";
++
++/* Options bit values, defined in <pcre.h>.  We don't include it here, because
++   it is not a standard header.  */
++#define PCRE_ANCHORED 0x00000010
++#define PCRE_EXTENDED 0x00000008
++
++struct regex_quote_spec
++regex_quote_spec_pcre (int options, bool anchored)
++{
++  struct regex_quote_spec result;
++  char *p;
++
++  p = result.special;
++  memcpy (p, bre_special, sizeof (pcre_special) - 1);
++  p += sizeof (pcre_special) - 1;
++  if (options & PCRE_EXTENDED)
++    {
++      *p++ = ' ';
++      *p++ = '\t';
++      *p++ = '\n';
++      *p++ = '\v';
++      *p++ = '\f';
++      *p++ = '\r';
++      *p++ = '#';
++    }
++  *p = '\0';
++
++  /* PCRE regular expressions consist of UTF-8 characters of options contains
++     PCRE_UTF8 and of single bytes otherwise.  */
++  result.multibyte = false;
++  /* If options contains PCRE_ANCHORED, the anchoring is implicit.  */
++  result.anchored = (options & PCRE_ANCHORED ? 0 : anchored);
++
++  return result;
++}
++
++size_t
++regex_quote_length (const char *string, const struct regex_quote_spec *spec)
++{
++  const char *special = spec->special;
++  size_t length;
++
++  length = 0;
++  if (spec->anchored)
++    length += 2; /* for '^' at the beginning and '$' at the end */
++  if (spec->multibyte)
++    {
++      mbui_iterator_t iter;
++
++      for (mbui_init (iter, string); mbui_avail (iter); mbui_advance (iter))
++        {
++          /* We know that special contains only ASCII characters.  */
++          if (mb_len (mbui_cur (iter)) == 1
++              && strchr (special, * mbui_cur_ptr (iter)))
++            length += 1;
++          length += mb_len (mbui_cur (iter));
++        }
++    }
++  else
++    {
++      const char *iter;
++
++      for (iter = string; *iter != '\0'; iter++)
++        {
++          if (strchr (special, *iter))
++            length += 1;
++          length += 1;
++        }
++    }
++
++  return length;
++}
++
++char *
++regex_quote_copy (char *p, const char *string, const struct regex_quote_spec *spec)
++{
++  const char *special = spec->special;
++
++  if (spec->anchored)
++    *p++ = '^';
++  if (spec->multibyte)
++    {
++      mbui_iterator_t iter;
++
++      for (mbui_init (iter, string); mbui_avail (iter); mbui_advance (iter))
++        {
++          /* We know that special contains only ASCII characters.  */
++          if (mb_len (mbui_cur (iter)) == 1
++              && strchr (special, * mbui_cur_ptr (iter)))
++            *p++ = '\\';
++          memcpy (p, mbui_cur_ptr (iter), mb_len (mbui_cur (iter)));
++          p += mb_len (mbui_cur (iter));
++        }
++    }
++  else
++    {
++      const char *iter;
++
++      for (iter = string; *iter != '\0'; iter++)
++        {
++          if (strchr (special, *iter))
++            *p++ = '\\';
++          *p++ = *iter++;
++        }
++    }
++  if (spec->anchored)
++    *p++ = '$';
++
++  return p;
++}
++
++char *
++regex_quote (const char *string, const struct regex_quote_spec *spec)
++{
++  size_t length = regex_quote_length (string, spec);
++  char *result = XNMALLOC (length + 1, char);
++  char *p;
++
++  p = result;
++  p = regex_quote_copy (p, string, spec);
++  *p = '\0';
++  return result;
++}
+--- origsrc/lib/regex-quote.h	1970-01-01 01:00:00.000000000 +0100
++++ src/lib/regex-quote.h	2013-06-27 18:05:27.112447751 +0200
+@@ -0,0 +1,88 @@
++/* Construct a regular expression from a literal string.
++   Copyright (C) 1995, 2010-2013 Free Software Foundation, Inc.
++   Written by Bruno Haible <haible@clisp.cons.org>, 2010.
++
++   This program is free software: you can redistribute it and/or modify
++   it under the terms of the GNU General Public License as published by
++   the Free Software Foundation; either version 3 of the License, or
++   (at your option) any later version.
++
++   This program is distributed in the hope that it will be useful,
++   but WITHOUT ANY WARRANTY; without even the implied warranty of
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
++   GNU General Public License for more details.
++
++   You should have received a copy of the GNU General Public License
++   along with this program.  If not, see <http://www.gnu.org/licenses/>.  */
++
++#ifndef _REGEX_QUOTE_H
++#define _REGEX_QUOTE_H
++
++#include <stddef.h>
++#include <stdbool.h>
++
++
++/* Specifies a quotation task for converting a fixed string to a regular
++   expression pattern.  */
++struct regex_quote_spec
++{
++  /* True if the regular expression pattern consists of multibyte characters
++     (in the encoding given by the LC_CTYPE category of the locale),
++     false if it consists of single bytes or UTF-8 characters.  */
++  unsigned int /*bool*/ multibyte : 1;
++  /* True if the regular expression pattern shall match only entire lines.  */
++  unsigned int /*bool*/ anchored : 1;
++  /* Set of characters that need to be escaped (all ASCII), as a
++     NUL-terminated string.  */
++  char special[30 + 1];
++};
++
++
++/* Creates a quotation task that produces a POSIX regular expression, that is,
++   a pattern that can be compiled with regcomp().
++   CFLAGS can be 0 or REG_EXTENDED.
++   If it is 0, the result is a Basic Regular Expression (BRE)
++   <http://www.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap09.html#tag_09_03>.
++   If it is REG_EXTENDED, the result is an Extended Regular Expression (ERE)
++   <http://www.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap09.html#tag_09_04>.
++   If ANCHORED is false, the regular expression will match substrings of lines.
++   If ANCHORED is true, it will match only complete lines,  */
++extern struct regex_quote_spec
++       regex_quote_spec_posix (int cflags, bool anchored);
++
++/* Creates a quotation task that produces a regular expression that can be
++   compiled with the GNU API function re_compile_pattern().
++   SYNTAX describes the syntax of the regular expression (such as
++   RE_SYNTAX_POSIX_BASIC, RE_SYNTAX_POSIX_EXTENDED, RE_SYNTAX_EMACS, all
++   defined in <regex.h>).  It must be the same value as 're_syntax_options'
++   at the moment of the re_compile_pattern() call.
++   If ANCHORED is false, the regular expression will match substrings of lines.
++   If ANCHORED is true, it will match only complete lines,  */
++extern struct regex_quote_spec
++       regex_quote_spec_gnu (unsigned long /*reg_syntax_t*/ syntax, bool anchored);
++
++/* Creates a quotation task that produces a PCRE regular expression, that is,
++   a pattern that can be compiled with pcre_compile().
++   OPTIONS is the same value as the second argument passed to pcre_compile().
++   If ANCHORED is false, the regular expression will match substrings of lines.
++   If ANCHORED is true, it will match only complete lines,  */
++extern struct regex_quote_spec
++       regex_quote_spec_pcre (int options, bool anchored);
++
++
++/* Returns the number of bytes needed for the quoted string.  */
++extern size_t
++       regex_quote_length (const char *string, const struct regex_quote_spec *spec);
++
++/* Copies the quoted string to p and returns the incremented p.
++   There must be room for regex_quote_length (string, spec) + 1 bytes at p.  */
++extern char *
++       regex_quote_copy (char *p,
++                         const char *string, const struct regex_quote_spec *spec);
++
++/* Returns the freshly allocated quoted string.  */
++extern char *
++       regex_quote (const char *string, const struct regex_quote_spec *spec);
++
++
++#endif /* _REGEX_QUOTE_H */
+--- origsrc/lib/regex.c	2012-12-22 14:21:52.000000000 +0100
++++ src/lib/regex.c	2013-06-27 18:05:27.138447639 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2003, 2005-2006, 2009-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ #ifndef _LIBC
+ # include <config.h>
+@@ -25,6 +24,7 @@
+ #  pragma GCC diagnostic ignored "-Wsuggest-attribute=pure"
+ # endif
+ # if (__GNUC__ == 4 && 3 <= __GNUC_MINOR__) || 4 < __GNUC__
++#  pragma GCC diagnostic ignored "-Wold-style-definition"
+ #  pragma GCC diagnostic ignored "-Wtype-limits"
+ # endif
+ #endif
+--- origsrc/lib/regex.h	2012-12-22 14:21:52.000000000 +0100
++++ src/lib/regex.h	2013-06-27 18:05:27.168447509 +0200
+@@ -1,23 +1,22 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Definitions for data structures and routines for the regular
+    expression library.
+-   Copyright (C) 1985, 1989-1993, 1995-1998, 2000-2003, 2005-2012
+-   Free Software Foundation, Inc.
++   Copyright (C) 1985, 1989-1993, 1995-1998, 2000-2003, 2005-2013 Free Software
++   Foundation, Inc.
+    This file is part of the GNU C Library.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ #ifndef _REGEX_H
+ #define _REGEX_H 1
+--- origsrc/lib/regex_internal.c	2012-12-22 14:21:52.000000000 +0100
++++ src/lib/regex_internal.c	2013-06-27 18:05:27.199447375 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ static void re_string_construct_common (const char *str, Idx len,
+ 					re_string_t *pstr,
+@@ -835,7 +834,7 @@ re_string_reconstruct (re_string_t *pstr
+ }
+ 
+ static unsigned char
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure))
+ re_string_peek_byte_case (const re_string_t *pstr, Idx idx)
+ {
+   int ch;
+@@ -975,7 +974,7 @@ re_node_set_alloc (re_node_set *set, Idx
+   set->alloc = size;
+   set->nelem = 0;
+   set->elems = re_malloc (Idx, size);
+-  if (BE (set->elems == NULL, 0))
++  if (BE (set->elems == NULL, 0) && (MALLOC_0_IS_NONNULL || size != 0))
+     return REG_ESPACE;
+   return REG_NOERROR;
+ }
+@@ -1355,7 +1354,7 @@ re_node_set_insert_last (re_node_set *se
+    Return true if SET1 and SET2 are equivalent.  */
+ 
+ static bool
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure))
+ re_node_set_compare (const re_node_set *set1, const re_node_set *set2)
+ {
+   Idx i;
+@@ -1370,7 +1369,7 @@ re_node_set_compare (const re_node_set *
+ /* Return (idx + 1) if SET contains the element ELEM, return 0 otherwise.  */
+ 
+ static Idx
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure))
+ re_node_set_contains (const re_node_set *set, Idx elem)
+ {
+   __re_size_t idx, right, mid;
+@@ -1444,11 +1443,9 @@ re_dfa_add_node (re_dfa_t *dfa, re_token
+   dfa->nodes[dfa->nodes_len] = token;
+   dfa->nodes[dfa->nodes_len].constraint = 0;
+ #ifdef RE_ENABLE_I18N
+-  {
+-  int type = token.type;
+   dfa->nodes[dfa->nodes_len].accept_mb =
+-    (type == OP_PERIOD && dfa->mb_cur_max > 1) || type == COMPLEX_BRACKET;
+-  }
++    ((token.type == OP_PERIOD && dfa->mb_cur_max > 1)
++     || token.type == COMPLEX_BRACKET);
+ #endif
+   dfa->nexts[dfa->nodes_len] = REG_MISSING;
+   re_node_set_init_empty (dfa->edests + dfa->nodes_len);
+--- origsrc/lib/regex_internal.h	2012-12-22 14:21:52.000000000 +0100
++++ src/lib/regex_internal.h	2013-06-27 18:05:27.230447242 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ #ifndef _REGEX_INTERNAL_H
+ #define _REGEX_INTERNAL_H 1
+@@ -28,21 +27,54 @@
+ #include <string.h>
+ 
+ #include <langinfo.h>
+-#ifndef _LIBC
+-# include "localcharset.h"
+-#endif
+ #include <locale.h>
+ #include <wchar.h>
+ #include <wctype.h>
+ #include <stdbool.h>
+ #include <stdint.h>
+-#if defined _LIBC
++
++#ifdef _LIBC
+ # include <bits/libc-lock.h>
++# define lock_define(name) __libc_lock_define (, name)
++# define lock_init(lock) (__libc_lock_init (lock), 0)
++# define lock_fini(lock) 0
++# define lock_lock(lock) __libc_lock_lock (lock)
++# define lock_unlock(lock) __libc_lock_unlock (lock)
++#elif defined GNULIB_LOCK
++# include "glthread/lock.h"
++  /* Use gl_lock_define if empty macro arguments are known to work.
++     Otherwise, fall back on less-portable substitutes.  */
++# if ((defined __GNUC__ && !defined __STRICT_ANSI__) \
++      || (defined __STDC_VERSION__ && 199901L <= __STDC_VERSION__))
++#  define lock_define(name) gl_lock_define (, name)
++# elif USE_POSIX_THREADS
++#  define lock_define(name) pthread_mutex_t name;
++# elif USE_PTH_THREADS
++#  define lock_define(name) pth_mutex_t name;
++# elif USE_SOLARIS_THREADS
++#  define lock_define(name) mutex_t name;
++# elif USE_WINDOWS_THREADS
++#  define lock_define(name) gl_lock_t name;
++# else
++#  define lock_define(name)
++# endif
++# define lock_init(lock) glthread_lock_init (&(lock))
++# define lock_fini(lock) glthread_lock_destroy (&(lock))
++# define lock_lock(lock) glthread_lock_lock (&(lock))
++# define lock_unlock(lock) glthread_lock_unlock (&(lock))
++#elif defined GNULIB_PTHREAD
++# include <pthread.h>
++# define lock_define(name) pthread_mutex_t name;
++# define lock_init(lock) pthread_mutex_init (&(lock), 0)
++# define lock_fini(lock) pthread_mutex_destroy (&(lock))
++# define lock_lock(lock) pthread_mutex_lock (&(lock))
++# define lock_unlock(lock) pthread_mutex_unlock (&(lock))
+ #else
+-# define __libc_lock_define(CLASS,NAME)
+-# define __libc_lock_init(NAME) do { } while (0)
+-# define __libc_lock_lock(NAME) do { } while (0)
+-# define __libc_lock_unlock(NAME) do { } while (0)
++# define lock_define(name)
++# define lock_init(lock) 0
++# define lock_fini(lock) 0
++# define lock_lock(lock) ((void) 0)
++# define lock_unlock(lock) ((void) 0)
+ #endif
+ 
+ /* In case that the system doesn't have isblank().  */
+@@ -65,7 +97,7 @@
+ # ifdef _LIBC
+ #  undef gettext
+ #  define gettext(msgid) \
+-  INTUSE(__dcgettext) (_libc_intl_domainname, msgid, LC_MESSAGES)
++  __dcgettext (_libc_intl_domainname, msgid, LC_MESSAGES)
+ # endif
+ #else
+ # define gettext(msgid) (msgid)
+@@ -101,6 +133,8 @@
+ 
+ /* Rename to standard API for using out of glibc.  */
+ #ifndef _LIBC
++# undef __wctype
++# undef __iswctype
+ # define __wctype wctype
+ # define __iswctype iswctype
+ # define __btowc btowc
+@@ -110,10 +144,8 @@
+ # define attribute_hidden
+ #endif /* not _LIBC */
+ 
+-#if __GNUC__ >= 4 || (__GNUC__ == 3 && __GNUC_MINOR__ >= 1)
+-# define __attribute(arg) __attribute__ (arg)
+-#else
+-# define __attribute(arg)
++#if __GNUC__ < 3 + (__GNUC_MINOR__ < 1)
++# define __attribute__(arg)
+ #endif
+ 
+ typedef __re_idx_t Idx;
+@@ -429,7 +461,7 @@ static void build_upper_buffer (re_strin
+ static void re_string_translate_buffer (re_string_t *pstr) internal_function;
+ static unsigned int re_string_context_at (const re_string_t *input, Idx idx,
+ 					  int eflags)
+-     internal_function __attribute ((pure));
++     internal_function __attribute__ ((pure));
+ #endif
+ #define re_string_peek_byte(pstr, offset) \
+   ((pstr)->mbs[(pstr)->cur_idx + offset])
+@@ -448,7 +480,9 @@ static unsigned int re_string_context_at
+ #define re_string_skip_bytes(pstr,idx) ((pstr)->cur_idx += (idx))
+ #define re_string_set_index(pstr,idx) ((pstr)->cur_idx = (idx))
+ 
+-#include <alloca.h>
++#if defined _LIBC || HAVE_ALLOCA
++# include <alloca.h>
++#endif
+ 
+ #ifndef _LIBC
+ # if HAVE_ALLOCA
+@@ -465,6 +499,12 @@ static unsigned int re_string_context_at
+ # endif
+ #endif
+ 
++#ifdef _LIBC
++# define MALLOC_0_IS_NONNULL 1
++#elif !defined MALLOC_0_IS_NONNULL
++# define MALLOC_0_IS_NONNULL 0
++#endif
++
+ #ifndef MAX
+ # define MAX(a,b) ((a) < (b) ? (b) : (a))
+ #endif
+@@ -695,7 +735,7 @@ struct re_dfa_t
+ #ifdef DEBUG
+   char* re_str;
+ #endif
+-  __libc_lock_define (, lock)
++  lock_define (lock)
+ };
+ 
+ #define re_node_set_init_empty(set) memset (set, '\0', sizeof (re_node_set))
+@@ -767,7 +807,7 @@ bitset_copy (bitset_t dest, const bitset
+   memcpy (dest, src, sizeof (bitset_t));
+ }
+ 
+-static void
++static void __attribute__ ((unused))
+ bitset_not (bitset_t set)
+ {
+   int bitset_i;
+@@ -779,7 +819,7 @@ bitset_not (bitset_t set)
+        & ~set[BITSET_WORDS - 1]);
+ }
+ 
+-static void
++static void __attribute__ ((unused))
+ bitset_merge (bitset_t dest, const bitset_t src)
+ {
+   int bitset_i;
+@@ -787,7 +827,7 @@ bitset_merge (bitset_t dest, const bitse
+     dest[bitset_i] |= src[bitset_i];
+ }
+ 
+-static void
++static void __attribute__ ((unused))
+ bitset_mask (bitset_t dest, const bitset_t src)
+ {
+   int bitset_i;
+@@ -798,7 +838,7 @@ bitset_mask (bitset_t dest, const bitset
+ #ifdef RE_ENABLE_I18N
+ /* Functions for re_string.  */
+ static int
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure, unused))
+ re_string_char_size_at (const re_string_t *pstr, Idx idx)
+ {
+   int byte_idx;
+@@ -811,7 +851,7 @@ re_string_char_size_at (const re_string_
+ }
+ 
+ static wint_t
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure, unused))
+ re_string_wchar_at (const re_string_t *pstr, Idx idx)
+ {
+   if (pstr->mb_cur_max == 1)
+@@ -821,7 +861,7 @@ re_string_wchar_at (const re_string_t *p
+ 
+ # ifndef NOT_IN_libc
+ static int
+-internal_function __attribute ((pure))
++internal_function __attribute__ ((pure, unused))
+ re_string_elem_size_at (const re_string_t *pstr, Idx idx)
+ {
+ #  ifdef _LIBC
+--- origsrc/lib/regexec.c	2012-12-22 14:21:52.000000000 +0100
++++ src/lib/regexec.c	2013-06-27 18:05:27.268447078 +0200
+@@ -1,22 +1,21 @@
+-/* -*- buffer-read-only: t -*- vi: set ro: */
+-/* DO NOT EDIT! GENERATED AUTOMATICALLY! */
+ /* Extended regular expression matching and search library.
+-   Copyright (C) 2002-2012 Free Software Foundation, Inc.
++   Copyright (C) 2002-2013 Free Software Foundation, Inc.
+    This file is part of the GNU C Library.
+    Contributed by Isamu Hasegawa <isamu@yamato.ibm.com>.
+ 
+-   This program is free software; you can redistribute it and/or modify
+-   it under the terms of the GNU General Public License as published by
+-   the Free Software Foundation; either version 3, or (at your option)
+-   any later version.
++   The GNU C Library is free software; you can redistribute it and/or
++   modify it under the terms of the GNU Lesser General Public
++   License as published by the Free Software Foundation; either
++   version 2.1 of the License, or (at your option) any later version.
+ 
+-   This program is distributed in the hope that it will be useful,
++   The GNU C Library is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+-   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+-   GNU General Public License for more details.
++   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
++   Lesser General Public License for more details.
+ 
+-   You should have received a copy of the GNU General Public License along
+-   with this program; if not, see <http://www.gnu.org/licenses/>.  */
++   You should have received a copy of the GNU Lesser General Public
++   License along with the GNU C Library; if not, see
++   <http://www.gnu.org/licenses/>.  */
+ 
+ static reg_errcode_t match_ctx_init (re_match_context_t *cache, int eflags,
+ 				     Idx n) internal_function;
+@@ -200,7 +199,7 @@ static Idx group_nodes_into_DFAstates (c
+ static bool check_node_accept (const re_match_context_t *mctx,
+ 			       const re_token_t *node, Idx idx)
+      internal_function;
+-static reg_errcode_t extend_buffers (re_match_context_t *mctx)
++static reg_errcode_t extend_buffers (re_match_context_t *mctx, int min_len)
+      internal_function;
+ 
+ /* Entry point for POSIX code.  */
+@@ -229,9 +228,7 @@ regexec (preg, string, nmatch, pmatch, e
+ {
+   reg_errcode_t err;
+   Idx start, length;
+-#ifdef _LIBC
+   re_dfa_t *dfa = preg->buffer;
+-#endif
+ 
+   if (eflags & ~(REG_NOTBOL | REG_NOTEOL | REG_STARTEND))
+     return REG_BADPAT;
+@@ -247,14 +244,14 @@ regexec (preg, string, nmatch, pmatch, e
+       length = strlen (string);
+     }
+ 
+-  __libc_lock_lock (dfa->lock);
++  lock_lock (dfa->lock);
+   if (preg->no_sub)
+     err = re_search_internal (preg, string, length, start, length,
+ 			      length, 0, NULL, eflags);
+   else
+     err = re_search_internal (preg, string, length, start, length,
+ 			      length, nmatch, pmatch, eflags);
+-  __libc_lock_unlock (dfa->lock);
++  lock_unlock (dfa->lock);
+   return err != REG_NOERROR;
+ }
+ 
+@@ -422,9 +419,7 @@ re_search_stub (struct re_pattern_buffer
+   Idx nregs;
+   regoff_t rval;
+   int eflags = 0;
+-#ifdef _LIBC
+   re_dfa_t *dfa = bufp->buffer;
+-#endif
+   Idx last_start = start + range;
+ 
+   /* Check for out-of-range.  */
+@@ -435,7 +430,7 @@ re_search_stub (struct re_pattern_buffer
+   else if (BE (last_start < 0 || (range < 0 && start <= last_start), 0))
+     last_start = 0;
+ 
+-  __libc_lock_lock (dfa->lock);
++  lock_lock (dfa->lock);
+ 
+   eflags |= (bufp->not_bol) ? REG_NOTBOL : 0;
+   eflags |= (bufp->not_eol) ? REG_NOTEOL : 0;
+@@ -499,7 +494,7 @@ re_search_stub (struct re_pattern_buffer
+     }
+   re_free (pmatch);
+  out:
+-  __libc_lock_unlock (dfa->lock);
++  lock_unlock (dfa->lock);
+   return rval;
+ }
+ 
+@@ -1065,7 +1060,7 @@ prune_impossible_nodes (re_match_context
+    since initial states may have constraints like "\<", "^", etc..  */
+ 
+ static inline re_dfastate_t *
+-__attribute ((always_inline)) internal_function
++__attribute__ ((always_inline)) internal_function
+ acquire_init_state_context (reg_errcode_t *err, const re_match_context_t *mctx,
+ 			    Idx idx)
+ {
+@@ -1177,7 +1172,7 @@ check_matching (re_match_context_t *mctx
+ 	  || (BE (next_char_idx >= mctx->input.valid_len, 0)
+ 	      && mctx->input.valid_len < mctx->input.len))
+ 	{
+-	  err = extend_buffers (mctx);
++	  err = extend_buffers (mctx, next_char_idx + 1);
+ 	  if (BE (err != REG_NOERROR, 0))
+ 	    {
+ 	      assert (err == REG_ESPACE);
+@@ -1757,7 +1752,7 @@ clean_state_log_if_needed (re_match_cont
+ 	  && mctx->input.valid_len < mctx->input.len))
+     {
+       reg_errcode_t err;
+-      err = extend_buffers (mctx);
++      err = extend_buffers (mctx, next_state_log_idx + 1);
+       if (BE (err != REG_NOERROR, 0))
+ 	return err;
+     }
+@@ -2814,7 +2809,7 @@ get_subexp (re_match_context_t *mctx, Id
+ 		  if (bkref_str_off >= mctx->input.len)
+ 		    break;
+ 
+-		  err = extend_buffers (mctx);
++		  err = extend_buffers (mctx, bkref_str_off + 1);
+ 		  if (BE (err != REG_NOERROR, 0))
+ 		    return err;
+ 
+@@ -3937,6 +3932,7 @@ check_node_accept_bytes (const re_dfa_t
+ 		in_collseq = find_collation_sequence_value (pin, elem_len);
+ 	    }
+ 	  /* match with range expression?  */
++	  /* FIXME: Implement rational ranges here, too.  */
+ 	  for (i = 0; i < cset->nranges; ++i)
+ 	    if (cset->range_starts[i] <= in_collseq
+ 		&& in_collseq <= cset->range_ends[i])
+@@ -3988,18 +3984,9 @@ check_node_accept_bytes (const re_dfa_t
+ # endif /* _LIBC */
+ 	{
+ 	  /* match with range expression?  */
+-#if __GNUC__ >= 2 && ! (__STDC_VERSION__ < 199901L && defined __STRICT_ANSI__)
+-	  wchar_t cmp_buf[] = {L'\0', L'\0', wc, L'\0', L'\0', L'\0'};
+-#else
+-	  wchar_t cmp_buf[] = {L'\0', L'\0', L'\0', L'\0', L'\0', L'\0'};
+-	  cmp_buf[2] = wc;
+-#endif
+ 	  for (i = 0; i < cset->nranges; ++i)
+ 	    {
+-	      cmp_buf[0] = cset->range_starts[i];
+-	      cmp_buf[4] = cset->range_ends[i];
+-	      if (wcscoll (cmp_buf, cmp_buf + 2) <= 0
+-		  && wcscoll (cmp_buf + 2, cmp_buf + 4) <= 0)
++	      if (cset->range_starts[i] <= wc && wc <= cset->range_ends[i])
+ 		{
+ 		  match_len = char_len;
+ 		  goto check_node_accept_bytes_match;
+@@ -4137,7 +4124,7 @@ check_node_accept (const re_match_contex
+ 
+ static reg_errcode_t
+ internal_function __attribute_warn_unused_result__
+-extend_buffers (re_match_context_t *mctx)
++extend_buffers (re_match_context_t *mctx, int min_len)
+ {
+   reg_errcode_t ret;
+   re_string_t *pstr = &mctx->input;
+@@ -4147,8 +4134,10 @@ extend_buffers (re_match_context_t *mctx
+           <= pstr->bufs_len, 0))
+     return REG_ESPACE;
+ 
+-  /* Double the lengths of the buffers.  */
+-  ret = re_string_realloc_buffers (pstr, MIN (pstr->len, pstr->bufs_len * 2));
++  /* Double the lengths of the buffers, but allocate at least MIN_LEN.  */
++  ret = re_string_realloc_buffers (pstr,
++				   MAX (min_len,
++					MIN (pstr->len, pstr->bufs_len * 2)));
+   if (BE (ret != REG_NOERROR, 0))
+     return ret;
+ 
+--- origsrc/sed/sed.c	2012-03-16 10:13:31.000000000 +0100
++++ src/sed/sed.c	2013-06-27 18:06:25.592195456 +0200
+@@ -57,7 +57,11 @@ bool follow_symlinks = false;
+ char *in_place_extension = NULL;
+ 
+ /* The mode to use to read/write files, either "r"/"w" or "rb"/"wb".  */
++#ifdef HAVE_FOPEN_RT
++char *read_mode = "rt";
++#else
+ char *read_mode = "r";
++#endif
+ char *write_mode = "w";
+ 
+ /* Do we need to be pedantically POSIX compliant? */
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index a0a4e0749..309050057 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -32,4 +32,4 @@ sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUt
 sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
 sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
 
-( cd ${Color_CI_DIR} && make -j ${NJOBS} )
+( cd ${Color_CI_DIR} && make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 5435e9588..238960948 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -68,7 +68,7 @@ install_ssreflect()
     sed -i.bak '/field/d'       Make && \
     sed -i.bak '/fingroup/d'    Make && \
     sed -i.bak '/algebra/d'     Make && \
-    make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install )
+    make Makefile.coq && make -f Makefile.coq all && make install )
 
   echo -en 'travis_fold:end:ssr.install\\r'
 
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index c78ffdc2c..0dd904648 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -9,4 +9,4 @@ opam install -j ${NJOBS} -y menhir
 git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
 
 # Patch to avoid the upper version limit
-( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} )
+( cd ${CompCert_CI_DIR} && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 0e791ebbf..8b725f6fe 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -6,5 +6,5 @@ source ${ci_dir}/ci-common.sh
 wget http://adam.chlipala.net/cpdt/cpdt.tgz
 tar xvfz cpdt.tgz
 
-( cd cpdt && make clean && make -j ${NJOBS} )
+( cd cpdt && make clean && make )
 
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index c6df45a1d..5ca3ac47f 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -6,5 +6,6 @@ source ${ci_dir}/ci-common.sh
 fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
 
 git_checkout ${fiat_crypto_CI_BRANCH} ${fiat_crypto_CI_GITURL} ${fiat_crypto_CI_DIR}
+( cd ${fiat_crypto_CI_DIR} && git submodule update --init --recursive )
 
-( cd ${fiat_crypto_CI_DIR} && make -j ${NJOBS} lite )
+( cd ${fiat_crypto_CI_DIR} && make lite )
diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat-parsers.sh
index 2095245eb..292331b81 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -7,4 +7,4 @@ fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
 
 git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
 
-( cd ${fiat_parsers_CI_DIR} && make -j ${NJOBS} parsers parsers-examples && make -j ${NJOBS} fiat-core )
+( cd ${fiat_parsers_CI_DIR} && make parsers parsers-examples && make fiat-core )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 64b78c039..2556f84a5 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -17,16 +17,16 @@ source ${ci_dir}/ci-bignums.sh
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
 
-( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+( cd ${math_classes_CI_DIR} && make && make install )
 
 # Setup Corn
 
 git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
 
-( cd ${Corn_CI_DIR} && make -j ${NJOBS} && make install )
+( cd ${Corn_CI_DIR} && make && make install )
 
 # Setup formal-topology
 
 git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR}
 
-( cd ${formal_topology_CI_DIR} && make -j ${NJOBS} )
+( cd ${formal_topology_CI_DIR} && make )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 4e5aa2687..eadeb7c38 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -13,4 +13,4 @@ git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
   sed -i.bak '/Elements\/Book_1\.v/d'                Make && \
   sed -i.bak '/Elements\/Book_3\.v/d'                Make && \
   coq_makefile -f Make -o Makefile                        && \
-  make -j ${NJOBS} )
+  make )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 1bf6e9a87..693135a4c 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
 
 git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
 
-( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} )
+( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make )
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh
index 262dd6fa0..2d127ddc1 100755
--- a/dev/ci/ci-iris-coq.sh
+++ b/dev/ci/ci-iris-coq.sh
@@ -20,7 +20,7 @@ stdpp_CI_COMMIT=${IRIS_DEP[2]}
 
 git_checkout ${stdpp_CI_BRANCH} ${stdpp_CI_GITURL} ${stdpp_CI_DIR} ${stdpp_CI_COMMIT}
 
-( cd ${stdpp_CI_DIR} && make -j ${NJOBS} && make install )
+( cd ${stdpp_CI_DIR} && make && make install )
 
 # Build iris now
-( cd ${Iris_CI_DIR} && make -j ${NJOBS} )
+( cd ${Iris_CI_DIR} && make )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 46581c638..2837dee96 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -15,10 +15,10 @@ source ${ci_dir}/ci-bignums.sh
 
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
 
-( cd ${math_classes_CI_DIR} && make -j ${NJOBS} && make install )
+( cd ${math_classes_CI_DIR} && make && make install )
 
 # Setup Corn
 
 git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
 
-( cd ${Corn_CI_DIR} && make -j ${NJOBS} )
+( cd ${Corn_CI_DIR} && make )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index bb8188da4..701403f2c 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -12,4 +12,4 @@ checkout_mathcomp ${mathcomp_CI_DIR}
 ( cd ${mathcomp_CI_DIR}/mathcomp                  && \
   sed -i.bak '/PFsection/d'                  Make && \
   sed -i.bak '/stripped_odd_order_theorem/d' Make && \
-  make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all )
+  make Makefile.coq && make -f Makefile.coq all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index e31691179..c813b1fe9 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -10,10 +10,10 @@ metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
 git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
 
-( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install )
+( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make && make install )
 
 # Setup MetaCoq
 
 git_checkout ${metacoq_CI_BRANCH} ${metacoq_CI_GITURL} ${metacoq_CI_DIR}
 
-( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} )
+( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make )
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 23ef41d2d..6e6c7012b 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -9,6 +9,6 @@ tar xvfz sf.tgz
 
 sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
 
-( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
+( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make )
 
 
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
index 700105aed..25da01a82 100755
--- a/dev/ci/ci-template.sh
+++ b/dev/ci/ci-template.sh
@@ -9,4 +9,4 @@ Template_CI_DIR=${CI_BUILD_DIR}/Template
 
 git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR}
 
-( cd ${Template_CI_DIR} && make -j ${NJOBS} )
+( cd ${Template_CI_DIR} && make )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index ce2639937..8ecd8c441 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -7,4 +7,4 @@ tlc_CI_DIR=${CI_BUILD_DIR}/tlc
 
 git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
 
-( cd ${tlc_CI_DIR} && make -j ${NJOBS} )
+( cd ${tlc_CI_DIR} && make )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 175b82b5f..66b56add7 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -10,5 +10,5 @@ git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
 ( cd ${UniMath_CI_DIR}                        && \
   sed -i.bak '/Folds/d'              Makefile && \
   sed -i.bak '/HomologicalAlgebra/d' Makefile && \
-  make -j ${NJOBS} BUILD_COQ=no )
+  make BUILD_COQ=no )
 
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index c11195185..27a336d80 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -10,4 +10,4 @@ git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR}
 
 # Targets are: msl veric floyd
 # Patch to avoid the upper version limit
-( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make -j ${NJOBS} )
+( cd ${VST_CI_DIR} && sed -i.bak 's/8.6$/8.6 or-else trunk/' Makefile && make )
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index acfc4bea9..5966ac468 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -554,7 +554,7 @@ more efficient resolution behavior (the option is off by default). When
 a solution to the typeclass goal of this class is found, we never
 backtrack on it, assuming that it is canonical.
 
-\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]}
+\subsection{\tt Typeclasses eauto := [debug] [(dfs) | (bfs)] [\emph{depth}]}
 \comindex{Typeclasses eauto}
 \label{TypeclassesEauto}
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 939fc87a6..f338c3055 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -38,21 +38,19 @@ construction allows defining ``signatures''.
 \end{figure}
 
 \noindent In the expression
-
-\smallskip
-{\tt Record} {\ident} {\params} \texttt{:} 
-   {\sort} := {\ident$_0$} \verb+{+
- {\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$}; 
-              \dots
-  {\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+.
-\smallskip
- 
+\begin{quote}
+{\tt Record {\ident} {\params} : {\sort} := {\ident$_0$} \{ \\
+  {\ident$_1$} \binders$_1$ : {\term$_1$} ; ... ; \\
+  {\ident$_n$} \binders$_n$ : {\term$_n$} \}.}
+\end{quote}
 \noindent the identifier {\ident} is the name of the defined record
 and {\sort} is its type. The identifier {\ident$_0$} is the name of
 its constructor. If {\ident$_0$} is omitted, the default name {\tt
-Build\_{\ident}} is used. If {\sort} is omitted, the default sort is ``{\Type}''.
-The identifiers {\ident$_1$}, ..,
-{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$}
+Build\_{\ident}} is used.
+If {\sort} is omitted, the default sort is {\Type}.
+The identifiers {\ident$_1$}, \dots, {\ident$_n$} are the names of
+fields and {\tt forall {\binders$_1$}, {\term$_1$}}, \dots,
+{\tt forall {\binders$_n$}, {\term$_n$}}
 their respective types. Remark that the type of {\ident$_i$} may
 depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the
 fields is important. Finally, {\params} are the parameters of the
@@ -82,26 +80,15 @@ Record Rat : Set := mkRat
     forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}.
 \end{coq_example}
 
-Remark here that the field
-\verb+Rat_cond+ depends on the field \verb+bottom+. 
-
-%Let us now see the work done by the {\tt Record} macro.
-%First the macro generates an inductive definition
-%with just one constructor:
-%
-%\medskip
-%\noindent
-%{\tt Inductive {\ident} \zeroone{\binders} : {\sort} := \\
-%\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. 
-%({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.}
-%\medskip
+Remark here that the field \verb+Rat_bottom_cond+ depends
+on the field \verb+bottom+ and \verb+Rat_irred_cond+ depends
+on both \verb+top+ and \verb+bottom+.
 
 Let us now see the work done by the {\tt Record} macro.  First the
 macro generates a variant type definition with just one constructor:
 \begin{quote}
-{\tt Variant {\ident} {\params} :{\sort} :=} \\
-\qquad {\tt
-  {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).}
+{\tt Variant {\ident} {\params} : {\sort} := \\
+  {\ident$_0$} ({\ident$_1$} : {\term$_1$}) ... ({\ident$_n$} : {\term$_n$}).}
 \end{quote}
 To build an object of type {\ident}, one should provide the
 constructor {\ident$_0$} with $n$ terms filling the fields of
@@ -109,28 +96,9 @@ the record.
 
 As an example, let us define the rational $1/2$:
 \begin{coq_example*}
-Require Import Arith.
 Theorem one_two_irred :
  forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1.
-\end{coq_example*}
-\begin{coq_eval}
-Lemma mult_m_n_eq_m_1 : forall m n:nat, m * n = 1 -> m = 1.
-destruct m; trivial.
-intros; apply f_equal with (f := S).
-destruct m; trivial.
-destruct n; simpl in H.
- rewrite <- mult_n_O in H.
-   discriminate.
- rewrite <- plus_n_Sm in H.
-   discriminate.
-Qed.
-
-intros x y z [H1 H2].
- apply mult_m_n_eq_m_1 with (n := y); trivial.
-\end{coq_eval}
-\ldots
-\begin{coq_example*}
-Qed.
+Admitted.
 \end{coq_example*}
 \begin{coq_example}
 Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
@@ -139,80 +107,6 @@ Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
 Check half.
 \end{coq_example}
 
-The macro generates also, when it is possible, the projection
-functions for destructuring an object of type {\ident}.  These
-projection functions have the same name that the corresponding
-fields. If a field is named ``\verb=_='' then no projection is built
-for it.  In our example:
-
-\begin{coq_example}
-Eval compute in half.(top).
-Eval compute in half.(bottom).
-Eval compute in half.(Rat_bottom_cond).
-\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-Records defined  with the {\tt Record}  keyword are not  allowed to be
-recursive (references  to the record's name  in the type  of its field
-raises an  error). To define recursive  records, one can  use the {\tt
-  Inductive} and {\tt CoInductive} keywords, resulting in an inductive
-or  co-inductive record.  A  \emph{caveat}, however,  is that  records
-cannot appear in mutually inductive (or co-inductive) definitions.
-Induction schemes are automatically generated for inductive records.
-Automatic generation of induction schemes for non-recursive records
-defined with the {\tt Record} keyword can be activated with the
-{\tt Nonrecursive Elimination Schemes} option
-(see~\ref{set-nonrecursive-elimination-schemes}).
-
-\begin{Warnings}
-\item {\tt {\ident$_i$} cannot be defined.}
-
-  It can happen that the definition of a projection is impossible.
-  This message is followed by an explanation of this impossibility.
-  There may be three reasons:
-   \begin{enumerate}
-   \item The name {\ident$_i$} already exists in the environment (see
-     Section~\ref{Axiom}).
-   \item The body of {\ident$_i$} uses an incorrect elimination for
-     {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}).
-   \item The type of the projections {\ident$_i$} depends on previous
-   projections which themselves could not be defined.
-   \end{enumerate}  
-\end{Warnings}     
-
-\begin{ErrMsgs}
-
-\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.}
-
-  The record name {\ident} appears in the type of its fields, but uses
-  the keyword  {\tt Record}. Use  the keyword {\tt Inductive}  or {\tt
-    CoInductive} instead.
-\item \errindex{Cannot handle mutually (co)inductive records.}
-
-  Records  cannot  be  defined  as  part  of  mutually  inductive  (or
-  co-inductive) definitions,  whether with records only  or mixed with
-  standard definitions.
-\item During the definition of the one-constructor inductive
-  definition, all the errors of inductive definitions, as described in
-  Section~\ref{gal-Inductive-Definitions}, may also occur.
-
-\end{ErrMsgs}
-
-\SeeAlso Coercions and records in Section~\ref{Coercions-and-records}
-of the chapter devoted to coercions.
-
-\Rem {\tt Structure} is a synonym of the keyword {\tt Record}.
-
-\Rem Creation of an object of record type can be done by calling {\ident$_0$}
-and passing arguments in the correct order.
-
-\begin{coq_example}
-Record point := { x : nat; y : nat }.
-Definition a := Build_point 5 3.
-\end{coq_example}
-
 \begin{figure}[t]
 \begin{centerframe}
 \begin{tabular}{lcl}
@@ -226,15 +120,17 @@ Definition a := Build_point 5 3.
 \label{fig:fieldsyntax}
 \end{figure}
 
-A syntax is available for creating objects by using named fields, as
+Alternatively, the following syntax allows creating objects by using named fields, as
 shown on Figure~\ref{fig:fieldsyntax}. The
 fields do not have to be in any particular order, nor do they have to be all
 present if the missing ones can be inferred or prompted for (see
 Section~\ref{Program}).
 
 \begin{coq_example}
-Definition b := {| x := 5; y := 3 |}.
-Definition c := {| y := 3; x := 5 |}.
+Definition half' :=
+  {| sign := true;
+     Rat_bottom_cond := O_S 1;
+     Rat_irred_cond := one_two_irred |}.
 \end{coq_example}
 
 This syntax can be disabled globally for printing by
@@ -256,23 +152,52 @@ This syntax can also be used for pattern matching.
 
 \begin{coq_example}
 Eval compute in (
-  match b with
-  | {| y := S n |} => n
+  match half with
+  | {| sign := true; top := n |} => n
   | _ => 0
   end).
 \end{coq_example}
 
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
+The macro generates also, when it is possible, the projection
+functions for destructuring an object of type {\ident}.  These
+projection functions are given the names of the corresponding
+fields. If a field is named ``\verb=_='' then no projection is built
+for it. In our example:
+
+\begin{coq_example}
+Eval compute in top half.
+Eval compute in bottom half.
+Eval compute in Rat_bottom_cond half.
+\end{coq_example}
+
+An alternative syntax for projections based on a dot notation is
+available:
+
+\begin{coq_example}
+Eval compute in half.(top).
+\end{coq_example}
 
-\Rem A syntax for projections based on a dot notation is
-available. The command to activate it is
+It can be activated for printing with the command
 \optindex{Printing Projections}
 \begin{quote}
 {\tt Set Printing Projections.}
 \end{quote}
 
+\begin{coq_example}
+Set Printing Projections.
+Check top half.
+\end{coq_example}
+
+The corresponding grammar rules are given in Figure~\ref{fig:projsyntax}.
+When {\qualid} denotes a projection, the syntax {\tt
+  {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax
+{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to
+{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax
+{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to
+{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term}
+is the object projected and the other arguments are the parameters of
+the inductive type.
+
 \begin{figure}[t]
 \begin{centerframe}
 \begin{tabular}{lcl}
@@ -285,18 +210,66 @@ available. The command to activate it is
 \label{fig:projsyntax}
 \end{figure}
 
-The corresponding grammar rules are given Figure~\ref{fig:projsyntax}.
-When {\qualid} denotes a projection, the syntax {\tt
-  {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax
-{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to
-{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax
-{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to
-{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term}
-is the object projected and the other arguments are the parameters of
-the inductive type.
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{Remarks}
+
+\item Records defined with the {\tt Record} keyword are not allowed to be
+recursive (references to the record's name in the type of its field
+raises an  error). To define recursive records, one can use the {\tt
+Inductive} and {\tt CoInductive} keywords, resulting in an inductive
+or co-inductive record.
+A \emph{caveat}, however, is that records
+cannot appear in mutually inductive (or co-inductive) definitions.
+
+\item Induction schemes are automatically generated for inductive records.
+Automatic generation of induction schemes for non-recursive records
+defined with the {\tt Record} keyword can be activated with the
+{\tt Nonrecursive Elimination Schemes} option
+(see~\ref{set-nonrecursive-elimination-schemes}).
+
+\item {\tt Structure} is a synonym of the keyword {\tt Record}.
 
-To deactivate the printing of projections, use 
-{\tt Unset Printing Projections}.
+\end{Remarks}
+
+\begin{Warnings}
+\item {\tt {\ident$_i$} cannot be defined.}
+
+  It can happen that the definition of a projection is impossible.
+  This message is followed by an explanation of this impossibility.
+  There may be three reasons:
+   \begin{enumerate}
+   \item The name {\ident$_i$} already exists in the environment (see
+     Section~\ref{Axiom}).
+   \item The body of {\ident$_i$} uses an incorrect elimination for
+     {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}).
+   \item The type of the projections {\ident$_i$} depends on previous
+   projections which themselves could not be defined.
+   \end{enumerate}  
+\end{Warnings}     
+
+\begin{ErrMsgs}
+
+\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.}
+
+  The record name {\ident} appears in the type of its fields, but uses
+  the keyword  {\tt Record}. Use  the keyword {\tt Inductive}  or {\tt
+    CoInductive} instead.
+\item \errindex{Cannot handle mutually (co)inductive records.}
+
+  Records  cannot  be  defined  as  part  of  mutually  inductive  (or
+  co-inductive) definitions,  whether with records only  or mixed with
+  standard definitions.
+\item During the definition of the one-constructor inductive
+  definition, all the errors of inductive definitions, as described in
+  Section~\ref{gal-Inductive-Definitions}, may also occur.
+
+\end{ErrMsgs}
+
+\SeeAlso Coercions and records in Section~\ref{Coercions-and-records}
+of the chapter devoted to coercions.
 
 \subsection{Primitive Projections}
 \optindex{Primitive Projections}
@@ -2011,6 +1984,11 @@ Check (fun x y => _) 0 1.
 Unset Printing Existential Instances.
 \end{coq_eval}
 
+Existential variables can be named by the user upon creation using
+the syntax {\tt ?[\ident]}. This is useful when the existential
+variable needs to be explicitly handled later in the script (e.g.
+with a named-goal selector, see~\ref{ltac:selector}).
+
 \subsection{Explicit displaying of existential instances for pretty-printing
 \label{SetPrintingExistentialInstances}
 \optindex{Printing Existential Instances}}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index bb679ecba..f3bc2dd05 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -392,7 +392,7 @@ all selected goals.
   \item{} [{\ident}] {\tt :} {\tacexpr}
 
     In this variant, {\tacexpr} is applied locally to a goal
-    previously named by the user.
+    previously named by the user (see~\ref{ExistentialVariables}).
 
   \item {\num} {\tt :} {\tacexpr}
 
@@ -891,7 +891,7 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag.
 
 \end{Variants}
 
-\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}
+\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal}
 \index{Ltac!match reverse goal@\texttt{match reverse goal}}
 \index{match goal@\texttt{match goal}!in Ltac}
 \index{match reverse goal@\texttt{match reverse goal}!in Ltac}}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index b66659dc8..95fee3241 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -421,6 +421,24 @@ This command displays the current goals.
 \item \errindex{No focused proof}
 \end{ErrMsgs}
 
+\item {\tt Show {\ident}.}\\
+  Displays the named goal {\ident}.
+  This is useful in particular to display a shelved goal but only works
+  if the corresponding existential variable has been named by the user
+  (see~\ref{ExistentialVariables}) as in the following example.
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\begin{coq_example*}
+Goal exists n, n = 0.
+  eexists ?[n].
+\end{coq_example*}
+\begin{coq_example}
+  Show n.
+\end{coq_example}
+
 \item {\tt Show Script.}\comindex{Show Script}\\
   Displays the whole list of tactics applied from the beginning
   of the current proof. 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index ecaf82806..d02b06df1 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -889,7 +889,8 @@ statically. For instance, if {\tt f} is a polymorphic function of type
 recognized as an argument to be interpreted in scope {\scope}.
 
 \comindex{Bind Scope}
-More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
+\label{bindscope}
+More generally, any coercion {\class} (see Chapter~\ref{Coercions-full}) can be
 bound to an interpretation scope. The command to do it is
 \begin{quote}
 {\tt Bind Scope} {\scope} \texttt{with} {\class}
@@ -908,7 +909,7 @@ Open Scope nat_scope. (* Define + on the nat as the default for + *)
 Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))).
 \end{coq_example}
 
-\Rem The scope {\tt type\_scope} has also a local effect on
+\Rem The scopes {\tt type\_scope} and {\tt function\_scope} also have a local effect on
 interpretation. See the next section.
 
 \SeeAlso The command to show the scopes bound to the arguments of a
@@ -940,10 +941,21 @@ Check # @@%mybool #.
 
 The scope {\tt type\_scope} has a special status. It is a primitive
 interpretation scope which is temporarily activated each time a
-subterm of an expression is expected to be a type. This includes goals
-and statements, types of binders, domain and codomain of implication,
-codomain of products, and more generally any type argument of a
-declared or defined constant.
+subterm of an expression is expected to be a type.  It is delimited by
+the key {\tt type}, and bound to the coercion class {\tt Sortclass}. It is also
+used in certain situations where an expression is statically known to
+be a type, including the conclusion and the type of hypotheses within
+an {\tt Ltac} goal match (see Section~\ref{ltac-match-goal})
+the statement of a theorem, the type of
+a definition, the type of a binder, the domain and codomain of
+implication, the codomain of products, and more generally any type
+argument of a declared or defined constant.
+
+\subsection[The {\tt function\_scope} interpretation scope]{The {\tt function\_scope} interpretation scope\index{function\_scope@\texttt{function\_scope}}}
+
+The scope {\tt function\_scope} also has a special status. 
+It is temporarily activated each time the argument of a global reference is
+recognized to be a {\tt Funclass instance}, i.e., of type {\tt forall x:A, B} or {\tt A -> B}.
 
 \subsection{Interpretation scopes used in the standard library of {\Coq}}
 
@@ -953,38 +965,39 @@ commands {\tt Print Scopes} or {\tt Print Scope {\scope}}.
 
 \subsubsection{\tt type\_scope}
 
-This includes infix {\tt *} for product types and infix {\tt +} for
-sum types. It is delimited by key {\tt type}.
+This scope includes infix {\tt *} for product types and infix {\tt +} for
+sum types. It is delimited by key {\tt type}, and bound to the coercion class 
+{\tt Sortclass}, as described at \ref{bindscope}.
 
 \subsubsection{\tt nat\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt nat}. Positive numerals in this scope are mapped to their
 canonical representent built from {\tt O} and {\tt S}. The scope is
-delimited by key {\tt nat}.
+delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}).
 
 \subsubsection{\tt N\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt N} (binary natural numbers). It is delimited by key {\tt N}
 and comes with an interpretation for numerals as closed term of type {\tt Z}.
 
 \subsubsection{\tt Z\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z} 
 and comes with an interpretation for numerals as closed term of type {\tt Z}.
 
 \subsubsection{\tt positive\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt positive} (binary strictly positive numbers). It is
 delimited by key {\tt positive} and comes with an interpretation for
 numerals as closed term of type {\tt positive}.
 
 \subsubsection{\tt Q\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt Q} (rational numbers defined as fractions of an integer and
 a strictly positive integer modulo the equality of the
 numerator-denominator cross-product). As for numerals, only $0$ and
@@ -993,13 +1006,13 @@ interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively).
 
 \subsubsection{\tt Qc\_scope}
 
-This includes the standard arithmetical operators and relations on the
+This scope includes the standard arithmetical operators and relations on the
 type {\tt Qc} of rational numbers defined as the type of irreducible
 fractions of an integer and a strictly positive integer.
 
 \subsubsection{\tt real\_scope}
 
-This includes the standard arithmetical operators and relations on
+This scope includes the standard arithmetical operators and relations on
 type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R}
 and comes with an interpretation for numerals as term of type {\tt
 R}. The interpretation is based on the binary decomposition.  The
@@ -1014,35 +1027,40 @@ those of {\tt R}.
 
 \subsubsection{\tt bool\_scope}
 
-This includes notations for the boolean operators. It is
-delimited by key {\tt bool}.
+This scope includes notations for the boolean operators. It is
+delimited by key {\tt bool}, and bound to the type {\tt bool} (see \ref{bindscope}).
 
 \subsubsection{\tt list\_scope}
 
-This includes notations for the list operators. It is
-delimited by key {\tt list}.
+This scope includes notations for the list operators. It is
+delimited by key {\tt list}, and bound to the type {\tt list} (see \ref{bindscope}).
+
+\subsubsection{\tt function\_scope}
+
+This scope is delimited by the key {\tt function}, and bound to the coercion class {\tt Funclass}, 
+as described at \ref{bindscope}.
 
 \subsubsection{\tt core\_scope}
 
-This includes the notation for pairs. It is delimited by key {\tt core}.
+This scope includes the notation for pairs. It is delimited by key {\tt core}.
 
 \subsubsection{\tt string\_scope}
 
-This includes notation for strings as elements of the type {\tt
+This scope includes notation for strings as elements of the type {\tt
 string}.  Special characters and escaping follow {\Coq} conventions
 on strings (see Section~\ref{strings}). Especially, there is no
 convention to visualize non printable characters of a string.  The
 file {\tt String.v} shows an example that contains quotes, a newline
-and a beep (i.e. the ascii character of code 7).
+and a beep (i.e. the ASCII character of code 7).
 
 \subsubsection{\tt char\_scope}
 
-This includes interpretation for all strings of the form
-\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form
+This scope includes interpretation for all strings of the form
+\verb!"!$c$\verb!"! where $c$ is an ASCII character, or of the form
 \verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly
 with leading 0's), or of the form \verb!""""!. Their respective
-denotations are the ascii code of $c$, the decimal ascii code $nnn$,
-or the ascii code of the character \verb!"! (i.e. the ascii code
+denotations are the ASCII code of $c$, the decimal ASCII code $nnn$,
+or the ASCII code of the character \verb!"! (i.e. the ASCII code
 34), all of them being represented in the type {\tt ascii}.
 
 \subsection{Displaying informations about scopes}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index be75dc9d5..4931ca3b6 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1515,23 +1515,33 @@ The {\tt evar} tactic creates a new local definition named \ident\ with
 type \term\ in the context. The body of this binding is a fresh
 existential variable.
 
-\subsection{\tt instantiate ( {\num} := {\term} )}
+\subsection{\tt instantiate ( {\ident} := {\term} )}
 \tacindex{instantiate}
 \label{instantiate}
 
 The {\tt instantiate} tactic refines (see Section~\ref{refine})
-an existential variable
-with the term \term. The \num\  argument is the position of the
-existential variable from right to left in the conclusion. This cannot be
-the number of the existential variable since this number is different
-in every session.
+an existential variable {\ident} with the term {\term}.
+It is equivalent to {\tt only [\ident]: refine \term} (preferred alternative).
 
-When you are referring to hypotheses which you did not name
+\begin{Remarks}
+\item To be able to refer to an existential variable by name, the
+user must have given the name explicitly (see~\ref{ExistentialVariables}).
+
+\item When you are referring to hypotheses which you did not name
 explicitly, be aware that Coq may make a different decision on how to
 name the variable in the current goal and in the context of the
 existential variable. This can lead to surprising behaviors.
+\end{Remarks}
 
 \begin{Variants}
+
+  \item {\tt instantiate ( {\num} := {\term} )}
+  This variant allows to refer to an existential variable which was not
+  named by the user. The {\num} argument is the position of the
+  existential variable from right to left in the goal.
+  Because this variant is not robust to slight changes in the goal,
+  its use is strongly discouraged.
+
   \item {\tt instantiate ( {\num} := {\term} ) in \ident}
 
   \item {\tt instantiate ( {\num} := {\term} ) in ( Value of {\ident} )}
diff --git a/engine/evd.ml b/engine/evd.ml
index ccce584bb..cfc9aa635 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -780,8 +780,9 @@ let new_sort_variable ?loc ?name rigid d =
 let add_global_univ d u =
   { d with universes = UState.add_global_univ d.universes u }
 
-let make_flexible_variable evd b u =
-  { evd with universes = UState.make_flexible_variable evd.universes b u }
+let make_flexible_variable evd ~algebraic u =
+  { evd with universes =
+      UState.make_flexible_variable evd.universes ~algebraic u }
 
 let make_evar_universe_context e l =
   let uctx = UState.make (Environ.universes e) in
diff --git a/engine/evd.mli b/engine/evd.mli
index 52327843c..3f00a3b0b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -522,7 +522,9 @@ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_
 val add_global_univ : evar_map -> Univ.Level.t -> evar_map
 
 val universe_rigidity : evar_map -> Univ.Level.t -> rigid
-val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map
+val make_flexible_variable : evar_map -> algebraic:bool -> Univ.universe_level -> evar_map
+(** See [UState.make_flexible_variable] *)
+
 val is_sort_variable : evar_map -> sorts -> Univ.universe_level option 
 (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is 
     not a local sort variable declared in [evm] *)
diff --git a/engine/uState.ml b/engine/uState.ml
index 0973ca457..63bd247d5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -384,16 +384,21 @@ let add_global_univ uctx u =
                                      uctx_initial_universes = initial;
                                      uctx_universes = univs }
 
-let make_flexible_variable ctx b u =
-  let {uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
+let make_flexible_variable ctx ~algebraic u =
+  let {uctx_local = cstrs; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} = ctx in
   let uvars' = Univ.LMap.add u None uvars in
   let avars' = 
-    if b then
+    if algebraic then
       let uu = Univ.Universe.make u in
       let substu_not_alg u' v =
         Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
       in
-        if not (Univ.LMap.exists substu_not_alg uvars)
+      let has_upper_constraint () =
+        Univ.Constraint.exists
+          (fun (l,d,r) -> d == Univ.Lt && Univ.Level.equal l u)
+          (Univ.ContextSet.constraints cstrs)
+      in
+        if not (Univ.LMap.exists substu_not_alg uvars || has_upper_constraint ())
         then Univ.LSet.add u avars else avars 
     else avars 
   in
diff --git a/engine/uState.mli b/engine/uState.mli
index 0cdc6277a..3776e4c9f 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -92,7 +92,14 @@ val emit_side_effects : Safe_typing.private_constants -> t -> t
 
 val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
 val add_global_univ : t -> Univ.Level.t -> t
-val make_flexible_variable : t -> bool -> Univ.Level.t -> t
+
+(** [make_flexible_variable g algebraic l]
+
+  Turn the variable [l] flexible, and algebraic if [algebraic] is true
+  and [l] can be. That is if there are no strict upper constraints on
+  [l] and and it does not appear in the instance of any non-algebraic
+  universe. Otherwise the variable is just made flexible. *)
+val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
 
 val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
 
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index d42364001..cb2b365a4 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -20,9 +20,8 @@ module CompactedDecl = Context.Compacted.Declaration
 
 (** Ide_slave : an implementation of [Interface], i.e. mainly an interp
     function and a rewind function. This specialized loop is triggered
-    when the -ideslave option is passed to Coqtop. Currently CoqIDE is
-    the only one using this mode, but we try here to be as generic as
-    possible, so this may change in the future... *)
+    when the -ideslave option is passed to Coqtop. *)
+
 
 (** Signal handling: we postpone ^C during input and output phases,
     but make it directly raise a Sys.Break during evaluation of the request. *)
@@ -65,7 +64,7 @@ let is_known_option cmd = match cmd with
 (** Check whether a command is forbidden in the IDE *)
 
 let ide_cmd_checks ~id (loc,ast) =
-  let user_error s = CErrors.user_err ?loc ~hdr:"CoqIde" (str s) in
+  let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in
   let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
   if is_debug ast then
     user_error "Debug mode not available in the IDE";
@@ -509,4 +508,4 @@ let () = Coqtop.toploop_run := loop
 
 let () = Usage.add_to_usage "coqidetop"
 "  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
-\n  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
+\n  --help-XML-protocol    print documentation of the Coq XML protocol\n"
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 95c03b9fc..7c251f79c 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -407,11 +407,15 @@ let opposite_tabs =
 let background_color =
   new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string)
 
+let attach_tag (pref : string preference) (tag : GText.tag) f =
+  tag#set_property (f pref#get);
+  pref#connect#changed ~callback:(fun c -> tag#set_property (f c))
+
 let attach_bg (pref : string preference) (tag : GText.tag) =
-  pref#connect#changed ~callback:(fun c -> tag#set_property (`BACKGROUND c))
+  attach_tag pref tag (fun c -> `BACKGROUND c)
 
 let attach_fg (pref : string preference) (tag : GText.tag) =
-  pref#connect#changed ~callback:(fun c -> tag#set_property (`FOREGROUND c))
+  attach_tag pref tag (fun c -> `FOREGROUND c)
 
 let processing_color =
   new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string)
diff --git a/interp/notation.ml b/interp/notation.ml
index f2b99513a..4067a6b94 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -582,11 +582,12 @@ let interpretation_eq (vars1, t1) (vars2, t2) =
   List.equal var_attributes_eq vars1 vars2 &&
   Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
 
-let exists_notation_in_scope scopt ntn r =
+let exists_notation_in_scope scopt ntn onlyprint r =
   let scope = match scopt with Some s -> s | None -> default_scope in
   try
     let sc = String.Map.find scope !scope_map in
     let n = String.Map.find ntn sc.notations in
+    onlyprint = n.not_onlyprinting && 
     interpretation_eq n.not_interp r
   with Not_found -> false
 
diff --git a/interp/notation.mli b/interp/notation.mli
index a1dcb2034..dd0144e8d 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -148,7 +148,7 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> boo
 
 (** Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
-      interpretation -> bool
+      bool -> interpretation -> bool
 
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 1931e8167..5d703011d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -22,9 +22,16 @@ open Notation_term
 (**********************************************************************)
 (* Utilities                                                          *)
 
+(* helper for NVar, NVar case in eq_notation_constr *)
+let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
+
 let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
 | NRef gr1, NRef gr2 -> eq_gr gr1 gr2
-| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2)
+| NVar id1, NVar id2 -> (
+   match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
+   | Some n,Some m -> Int.equal n m
+   | None  ,None   -> Id.equal id1 id2
+   | _             -> false)
 | NApp (t1, a1), NApp (t2, a2) ->
   (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
 | NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index a9849819b..ff7145267 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -35,28 +35,6 @@ let add_warning_in_category ~name ~category =
   in
   Hashtbl.replace categories category (name::ws)
 
-let create ~name ~category ?(default=Enabled) pp =
-  Hashtbl.add warnings name { default; category; status = default };
-  add_warning_in_category ~name ~category;
-  if default <> Disabled then
-    add_warning_in_category ~name ~category:"default";
-  fun ?loc x ->
-           let w = Hashtbl.find warnings name in
-           let loc = Option.append loc !current_loc in
-           match w.status with
-           | Disabled -> ()
-           | AsError -> CErrors.user_err ?loc (pp x)
-           | Enabled ->
-              let msg =
-                pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
-                  str category ++ str "]"
-              in
-              Feedback.msg_warning ?loc msg
-
-let warn_unknown_warning =
-  create ~name:"unknown-warning" ~category:"toplevel"
-         (fun name -> strbrk "Unknown warning name: " ++ str name)
-
 let set_warning_status ~name status =
   try
     let w = Hashtbl.find warnings name in 
@@ -111,12 +89,6 @@ let set_status ~name status =
 let split_flags s =
   let reg = Str.regexp "[ ,]+" in Str.split reg s
 
-let check_warning ~silent (_status,name) =
-  is_all_keyword name ||
-  Hashtbl.mem categories name ||
-  Hashtbl.mem warnings name ||
-  (if not silent then warn_unknown_warning name; false)
-
 (** [cut_before_all_rev] removes all flags subsumed by a later occurrence of the
     "all" flag, and reverses the list. *)
 let rec cut_before_all_rev acc = function
@@ -143,10 +115,9 @@ let uniquize_flags_rev flags =
     | [] -> acc
   in aux [] CString.Set.empty flags
 
-(** [normalize_flags] removes unknown or redundant warnings. If [silent] is
-    true, it emits a warning when an unknown warning is met. *)
+(** [normalize_flags] removes redundant warnings. Unknown warnings are kept
+    because they may be declared in a plugin that will be linked later. *)
 let normalize_flags ~silent warnings =
-  let warnings = List.filter (check_warning ~silent) warnings in
   let warnings = cut_before_all_rev warnings in
   uniquize_flags_rev warnings
 
@@ -179,3 +150,27 @@ let parse_flags s =
 
 let set_flags s =
   reset_default_warnings (); let s = parse_flags s in flags := s
+
+(* Adds a warning to the [warnings] and [category] tables. We then reparse the
+   warning flags string, because the warning being created might have been set
+   already. *)
+let create ~name ~category ?(default=Enabled) pp =
+  Hashtbl.replace warnings name { default; category; status = default };
+  add_warning_in_category ~name ~category;
+  if default <> Disabled then
+    add_warning_in_category ~name ~category:"default";
+  (* We re-parse and also re-normalize the flags, because the category of the
+     new warning is now known. *)
+  set_flags !flags;
+  fun ?loc x ->
+           let w = Hashtbl.find warnings name in
+           let loc = Option.append loc !current_loc in
+           match w.status with
+           | Disabled -> ()
+           | AsError -> CErrors.user_err ?loc (pp x)
+           | Enabled ->
+              let msg =
+                pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
+                  str category ++ str "]"
+              in
+              Feedback.msg_warning ?loc msg
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 92d78f6b2..9f4829761 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -70,7 +70,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
 	       else t
 	    | UnivFlexible alg ->
 	       if onlyalg && alg then
-	         (evdref := Evd.make_flexible_variable !evdref false l; t)
+	         (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t)
 	       else t))
       | Prop Pos when refreshset && not direction ->
        (* Cannot make a universe "lower" than "Set",
diff --git a/test-suite/bugs/closed/5205.v b/test-suite/bugs/closed/5205.v
new file mode 100644
index 000000000..406f37a4b
--- /dev/null
+++ b/test-suite/bugs/closed/5205.v
@@ -0,0 +1,6 @@
+Definition foo (n : nat) (m : nat) : nat := m.
+
+Arguments foo {_} _, _ _.
+
+Check foo 1 1.
+Check foo (n:=1) 1.
diff --git a/test-suite/bugs/closed/5365.v b/test-suite/bugs/closed/5365.v
new file mode 100644
index 000000000..be360d24d
--- /dev/null
+++ b/test-suite/bugs/closed/5365.v
@@ -0,0 +1,13 @@
+
+Inductive TupleT : nat -> Type :=
+| nilT : TupleT 0
+| consT {n} A : (A -> TupleT n) -> TupleT (S n).
+
+Inductive Tuple : forall n, TupleT n -> Type :=
+  nil : Tuple _ nilT
+| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F).
+
+Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type :=
+  tmNil : TupleMap _ nilT nilT
+| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n)
+  : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G).
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 2ccca829d..b9985a594 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -1,3 +1,14 @@
+(* Bug 5568, don't warn for notations in repeated module import *)
+
+Module foo.
+Notation compose := (fun g f => g f).
+Notation "g & f" := (compose g f) (at level 10).
+End foo.
+
+Import foo.
+Import foo.
+Import foo.
+
 (**********************************************************************)
 (* Notations for if and let (submitted by Roland Zumkeller)           *)
 
diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test-suite/output/RecognizePluginWarning.out
diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v
new file mode 100644
index 000000000..cd667bbd0
--- /dev/null
+++ b/test-suite/output/RecognizePluginWarning.v
@@ -0,0 +1,5 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *)
+
+(* Test that mentioning a warning defined in plugins works. The failure
+mode here is that these result in a warning about unknown warnings, since the
+plugins are not known at command line parsing time. *)
diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out
new file mode 100644
index 000000000..47409f3ec
--- /dev/null
+++ b/test-suite/output/UsePluginWarning.out
@@ -0,0 +1 @@
+type foo = __
diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v
new file mode 100644
index 000000000..c6e005464
--- /dev/null
+++ b/test-suite/output/UsePluginWarning.v
@@ -0,0 +1,7 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *)
+
+Require Extraction.
+Axiom foo : Prop.
+
+Extraction foo.
+
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index b800953b8..8eeb59898 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -46,10 +46,9 @@
 }
 
 let space = [' ' '\t' '\n' '\r']
-let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
-let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
-let identchar =
-  ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let lowercase = ['a'-'z']
+let uppercase = ['A'-'Z']
+let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9']
 let caml_up_ident = uppercase identchar*
 let caml_low_ident = lowercase identchar*
 
diff --git a/tools/ocamllibdep.mll b/tools/ocamllibdep.mll
index 5d11e3008..308bb582a 100644
--- a/tools/ocamllibdep.mll
+++ b/tools/ocamllibdep.mll
@@ -20,10 +20,9 @@
 }
 
 let space = [' ' '\t' '\n' '\r']
-let lowercase = ['a'-'z' '\223'-'\246' '\248'-'\255']
-let uppercase = ['A'-'Z' '\192'-'\214' '\216'-'\222']
-let identchar =
-  ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let lowercase = ['a'-'z']
+let uppercase = ['A'-'Z']
+let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9']
 let caml_up_ident = uppercase identchar*
 let caml_low_ident = lowercase identchar*
 
diff --git a/vernac/command.ml b/vernac/command.ml
index 0a82a945a..e04bebe33 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -383,7 +383,7 @@ let make_conclusion_flexible evdref ty poly =
       | Type u -> 
         (match Univ.universe_level u with
         | Some u -> 
-	  evdref := Evd.make_flexible_variable !evdref true u
+	  evdref := Evd.make_flexible_variable !evdref ~algebraic:true u
 	| None -> ())
       | _ -> ()
   else () 
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index ae662d74b..567fc57fa 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1164,11 +1164,11 @@ let open_notation i (_, nobj) =
   let scope = nobj.notobj_scope in
   let (ntn, df) = nobj.notobj_notation in
   let pat = nobj.notobj_interp in
-  let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in
+  let onlyprint = nobj.notobj_onlyprint  in
+  let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
   let active = is_active_compat nobj.notobj_compat in
   if Int.equal i 1 && fresh && active then begin
     (* Declare the interpretation *)
-    let onlyprint = nobj.notobj_onlyprint  in
     let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
     (* Declare the uninterpretation *)
     if not nobj.notobj_onlyparse then
diff --git a/vernac/record.ml b/vernac/record.ml
index 218cf7a0a..d61f44cac 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -124,7 +124,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
             let s' = EConstr.ESorts.kind !evars s' in
 	    (if poly then
                match Evd.is_sort_variable !evars s' with
-	       | Some l -> evars := Evd.make_flexible_variable !evars true l; 
+	       | Some l -> evars := Evd.make_flexible_variable !evars ~algebraic:true l; 
 	                  s, s', true
 	       | None -> s, s', false
              else s, s', false)