Improve shell scripts

48 files changed, 293 insertions, 383 deletions

diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index dc33838f1..c450e8157 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -10,19 +10,19 @@ VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
 APP=bin/CoqIDE_${VERSION}.app
 
 # Create a .app file with CoqIDE, without signing it
-make PRIVATEBINARIES=$APP -j $NJOBS -l2 $APP
+make PRIVATEBINARIES="$APP" -j "$NJOBS" -l2 "$APP"
 
 # Add Coq to the .app file
-make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
+make OLDROOT="$OUTDIR" COQINSTALLPREFIX="$APP/Contents/Resources/" install-coq install-ide-toploop
 
 # Create the dmg bundle
-mkdir -p $DMGDIR
-ln -sf /Applications $DMGDIR/Applications
-cp -r $APP $DMGDIR
+mkdir -p "$DMGDIR"
+ln -sf /Applications "$DMGDIR/Applications"
+cp -r "$APP" "$DMGDIR"
 
 mkdir -p _build
 
 # Temporary countermeasure to hdiutil error 5341
 # head -c9703424 /dev/urandom > $DMGDIR/.padding
 
-hdiutil create -imagekey zlib-level=9 -volname coq-$VERSION-installer-macos -srcfolder $DMGDIR -ov -format UDZO _build/coq-$VERSION-installer-macos.dmg
+hdiutil create -imagekey zlib-level=9 -volname "coq-$VERSION-installer-macos" -srcfolder "$DMGDIR" -ov -format UDZO "_build/coq-$VERSION-installer-macos.dmg"
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 16c972e80..7e606b554 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -14,30 +14,30 @@
 rcfile=~/.bash_profile
 donefile=~/.bash_profile.upated
 
+# to learn about `exec >> $file`, see https://www.tldp.org/LDP/abs/html/x17974.html
+exec >> $rcfile
+
 if [ ! -f $donefile ] ; then
 
-    echo >> $rcfile
-    
-    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
+    if [ "$1" != "" ] && [ "$1" != " " ]; then
+      echo export http_proxy="http://$1"
+      echo export https_proxy="http://$1"
+      echo export ftp_proxy="http://$1"
     fi
-    
-    mkdir -p $RESULT_INSTALLDIR_CFMT/bin
+
+    mkdir -p "$RESULT_INSTALLDIR_CFMT/bin"
 
     # A tightly controlled path helps to avoid issues
     # Note: the order is important: first have the cygwin binaries, then the mingw binaries in the path!
     # Note: /bin is mounted at /usr/bin and /lib at /usr/lib and it is common to use /usr/bin in PATH
     # See cat /proc/mounts
-    echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows" >> $rcfile
+    echo "export PATH=/usr/local/bin:/usr/bin:$RESULT_INSTALLDIR_CFMT/bin:/usr/$TARGET_ARCH/sys-root/mingw/bin:/cygdrive/c/Windows/system32:/cygdrive/c/Windows"
 
     # find and xargs complain if the environment is larger than (I think) 8k.
     # ORIGINAL_PATH (set by cygwin) can be a few k and exceed the limit
-    echo unset ORIGINAL_PATH >> $rcfile
-    
+    echo unset ORIGINAL_PATH
     # Other installations of OCaml will mess up things
-    echo unset OCAMLLIB >> $rcfile
+    echo unset OCAMLLIB
 
     touch $donefile
 fi
diff --git a/dev/build/windows/difftar-folder.sh b/dev/build/windows/difftar-folder.sh
index cbcf14ec2..3bba451ec 100644
--- a/dev/build/windows/difftar-folder.sh
+++ b/dev/build/windows/difftar-folder.sh
@@ -42,7 +42,7 @@ fi
 if [ "$strip" -gt 0 ] ; then
   # 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)/
+  prefix=$(tar -t -f "$tarfile" | head -1 | cut -d / -f -$strip)/
 else
   prefix=
 fi
@@ -60,13 +60,13 @@ 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
+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
@@ -76,14 +76,14 @@ tar --diff -a -f "$tarfile" --strip $strip --directory "$folder" | grep "Mod tim
   # Substitute ': Mod time differs' with nothing
   file=${file/: Mod time differs/}
   # Check if file exists
-  if [ -f "$folder/$file" ] ; then 
+  if [ -f "$folder/$file" ] ; then
     # Extract original file
     tar -x -a -f "$tarfile" --strip $strip --directory "$orig" "$prefix$file"
     # Compute diff
-    diff -u "$orig/$file" "$folder/$file" 
+    diff -u "$orig/$file" "$folder/$file"
   fi
 done
 
 if [ -d "$new" ] ; then
-  diff -u -r --unidirectional-new-file $empty $new
+  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 8e0d2341d..e5a7b04a1 100644
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -67,7 +67,7 @@ RMDIR_BEFORE_BUILD=1
 ###################### ARCHITECTURES #####################
 
 # The OS on which the build of the tool/lib runs
-BUILD=`gcc -dumpmachine`
+BUILD=$(gcc -dumpmachine)
 
 # The OS on which the tool runs
 # "`find /bin -name "*mingw32-gcc.exe"`" -dumpmachine
@@ -132,34 +132,34 @@ CYGWIN_REPO_FOLDER=${CYGWIN_REPO_FOLDER//\//%2f}
 # Copy files
 cp "$CYGWIN_LOCAL_CACHE_WFMT/$CYGWIN_REPO_FOLDER/$CYGWINARCH/setup.ini" $TARBALLS
 cp /etc/setup/installed.db $TARBALLS
-  
+
 ###################### LOGGING #####################
 
 # The folder which receives log files
 mkdir -p buildlogs
-LOGS=`pwd`/buildlogs
+LOGS=$(pwd)/buildlogs
 
 # The current log target (first part of the log file name)
 LOGTARGET=other
 
 log1() {
-  "$@" > $LOGS/$LOGTARGET-$1.log 2> $LOGS/$LOGTARGET-$1.err
+  "$@" > "$LOGS/$LOGTARGET-$1.log" 2> "$LOGS/$LOGTARGET-$1.err"
 }
 
 log2() {
-  "$@" > $LOGS/$LOGTARGET-$1-$2.log 2> $LOGS/$LOGTARGET-$1-$2.err
+  "$@" > "$LOGS/$LOGTARGET-$1-$2.log" 2> "$LOGS/$LOGTARGET-$1-$2.err"
 }
 
 log_1_3() {
-  "$@" > $LOGS/$LOGTARGET-$1-$3.log 2> $LOGS/$LOGTARGET-$1-$3.err
+  "$@" > "$LOGS/$LOGTARGET-$1-$3.log" 2> "$LOGS/$LOGTARGET-$1-$3.err"
 }
 
 logn() {
   LOGTARGETEX=$1
   shift
-  "$@" > $LOGS/$LOGTARGET-$LOGTARGETEX.log 2> $LOGS/$LOGTARGET-$LOGTARGETEX.err
+  "$@" > "$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
@@ -183,7 +183,7 @@ logn() {
 # - create build folder
 # - extract source archive
 # - patch source file if patch exists
-# 
+#
 # Parameters
 # $1 file server name including protocol prefix
 # $2 file name (without extension)
@@ -206,68 +206,68 @@ function get_expand_source_tar {
   else
     name=$2
   fi
-  
+
   if [ "$#" -ge 6 ] ; then
     folder=$6
   else
     folder=$name
   fi
-  
+
   # Set logging target
   logtargetold=$LOGTARGET
   LOGTARGET=$name
-  
+
   # Get the source archive either from the source cache or online
-  if [ ! -f $TARBALLS/$name.$3 ] ; then
+  if [ ! -f "$TARBALLS/$name.$3" ] ; then
     if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" ] ; then
-      cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS
+      cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" "$TARBALLS"
     else
-      wget $1/$2.$3
-      if file -i $2.$3 | grep text/html; then
-        echo Download failed: $1/$2.$3
+      wget "$1/$2.$3"
+      if file -i "$2.$3" | grep text/html; then
+        echo Download failed: "$1/$2.$3"
         echo The file wget downloaded is an html file:
-        cat $2.$3
+        cat "$2.$3"
         exit 1
       fi
       if [ ! "$2.$3" == "$name.$3" ] ; then
-        mv $2.$3 $name.$3
+        mv "$2.$3" "$name.$3"
       fi
-      mv $name.$3 $TARBALLS
+      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"
+        cp "$TARBALLS/$name.$3" "$SOURCE_LOCAL_CACHE_CFMT"
       fi
     fi
   fi
-  
+
   # Remove build directory (clean build)
   if [ $RMDIR_BEFORE_BUILD -eq 1 ] ; then
-    rm -f -r $folder
+    rm -f -r "$folder"
   fi
-  
+
   # Create build directory and cd
-  mkdir -p $folder
-  cd $folder
-  
+  mkdir -p "$folder"
+  cd "$folder"
+
   # Extract source archive
   if [ "$3" == "zip" ] ; then
-    log1 unzip $TARBALLS/$name.$3
+    log1 unzip "$TARBALLS/$name.$3"
     if [ "$strip" == "1" ] ; then
       # Ok, this is dirty, but it works and it fails if there are name clashes
-      mv */* .
+      mv -- */* .
     else
       echo "Unzip strip count not supported"
       return 1
     fi
   else
-    logn untar tar xvaf $TARBALLS/$name.$3 --strip $strip
+    logn untar tar xvaf "$TARBALLS/$name.$3" --strip $strip
   fi
-  
+
   # Patch if patch file exists
-  if [ -f $PATCHES/$name.patch ] ; then
-    log1 patch -p1 -i $PATCHES/$name.patch
+  if [ -f "$PATCHES/$name.patch" ] ; then
+    log1 patch -p1 -i "$PATCHES/$name.patch"
   fi
-  
+
   # Go back to base folder
   cd ..
 
@@ -283,7 +283,7 @@ function get_expand_source_tar {
 # - cd to build folder and extract source archive
 # - create bin_special subfolder and add it to $PATH
 # - remember things for build_post
-# 
+#
 # Parameters
 # $1 file server name including protocol prefix
 # $2 file name (without extension)
@@ -305,27 +305,27 @@ function build_prep {
   else
     name=$2
   fi
-  
+
   # Check if build is already done
-  if [ ! -f flagfiles/$name.finished ] ; then
+  if [ ! -f "flagfiles/$name.finished" ] ; then
     BUILD_PACKAGE_NAME=$name
     BUILD_OLDPATH=$PATH
-    BUILD_OLDPWD=`pwd`
+    BUILD_OLDPWD=$(pwd)
     LOGTARGET=$name
 
-    touch flagfiles/$name.started
-    
-    get_expand_source_tar $1 $2 $3 $strip $name
-    
-    cd $name
-    
+    touch "flagfiles/$name.started"
+
+    get_expand_source_tar "$1" "$2" "$3" "$strip" "$name"
+
+    cd "$name"
+
     # Create a folder and add it to path, where we can put special binaries
     # The path is restored in build_post
     mkdir bin_special
-    PATH=`pwd`/bin_special:$PATH
-    
+    PATH=$(pwd)/bin_special:$PATH
+
     return 0
-  else  
+  else
     return 1
   fi
 }
@@ -337,9 +337,9 @@ function build_prep {
 # ------------------------------------------------------------------------------
 
 function build_post {
-  if [ ! -f flagfiles/$BUILD_PACKAGE_NAME.finished ]; then
-    cd $BUILD_OLDPWD
-    touch flagfiles/$BUILD_PACKAGE_NAME.finished
+  if [ ! -f "flagfiles/$BUILD_PACKAGE_NAME.finished" ]; then
+    cd "$BUILD_OLDPWD"
+    touch "flagfiles/$BUILD_PACKAGE_NAME.finished"
     PATH=$BUILD_OLDPATH
     LOGTARGET=other
   fi
@@ -362,9 +362,10 @@ function build_post {
 # ------------------------------------------------------------------------------
 
 function build_conf_make_inst {
-  if build_prep $1 $2 $3 ; then
+  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}"
+    # shellcheck disable=SC2086
     log1 make $MAKE_OPT
     log2 make install
     log2 make clean
@@ -383,6 +384,7 @@ function build_conf_make_inst {
 function install_glob {
   # Check if any files matching the pattern exist
   if [ "$(echo $1)" != "$1" ] ; then
+    # shellcheck disable=SC2086
     install -D -t $2 $1
   fi
 }
@@ -398,7 +400,7 @@ function install_glob {
 # ------------------------------------------------------------------------------
 
 function install_rec {
-  ( cd $1 && find -type f -name "$2" -exec install -D -T  $1/{} $3/{} \; )
+  ( cd "$1" && find . -type f -name "$2" -exec install -D -T  "$1"/{} "$3"/{} \; )
 }
 
 # ------------------------------------------------------------------------------
@@ -411,7 +413,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
 }
 
@@ -439,7 +441,7 @@ function diff_files {
 # ------------------------------------------------------------------------------
 
 function filter_files {
-  egrep "$3" "/build/filelists/$2" > "/build/filelists/$1"
+  grep -E "$3" "/build/filelists/$2" > "/build/filelists/$1"
 }
 
 # ------------------------------------------------------------------------------
@@ -453,7 +455,7 @@ function files_to_nsis {
   # Split the path in the file list into path and filename and create SetOutPath and File instructions
   # Note: File /oname cannot be used, because it does not create the paths as SetOutPath does
   # Note: I didn't check if the redundant SetOutPath instructions have a bad impact on installer size or install time
-  cat "/build/filelists/$1" | tr '/' '\\' | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
+  tr '/' '\\' < "/build/filelists/$1" | sed -r 's/^\.(.*)\\([^\\]+)$/SetOutPath $INSTDIR\\\1\nFile ${COQ_SRC_PATH}\\\1\\\2/' > "/build/filelists/$1.nsh"
 }
 
 
@@ -501,7 +503,7 @@ function make_fontconfig {
   make_freetype
   make_expat
   # CONFIGURE PARAMETERS
-  # build/install fails without --disable-docs 
+  # build/install fails without --disable-docs
   build_conf_make_inst  http://www.freedesktop.org/software/fontconfig/release  fontconfig-2.11.94  tar.gz  true  --disable-docs
 }
 
@@ -532,7 +534,7 @@ function make_ncurses {
   #
   # CONFIGURE PARAMETERS
   # --enable-term-driver --enable-sp-funcs is rewuired for mingw (see README.MinGW)
-  # additional changes 
+  # additional changes
   # ADD --with-pkg-config
   # ADD --enable-pc-files
   # ADD --without-manpages
@@ -604,7 +606,7 @@ function make_gdk-pixbuf {
   # CONFIGURE PARAMETERS
   # --with-included-loaders=yes statically links the image file format handlers
   # This avoids "Cannot open pixbuf loader module file '/usr/x86_64-w64-mingw32/sys-root/mingw/lib/gdk-pixbuf-2.0/2.10.0/loaders.cache': No such file or directory"
-  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32  gdk-pixbuf-2.32.1  tar.xz  true  --with-included-loaders=yes 
+  build_conf_make_inst  http://ftp.gnome.org/pub/GNOME/sources/gdk-pixbuf/2.32  gdk-pixbuf-2.32.1  tar.xz  true  --with-included-loaders=yes
 }
 
 ##### CAIRO #####
@@ -657,8 +659,8 @@ function make_gtk3 {
   build_conf_make_inst  http://ftp.gnome.org/pub/gnome/sources/gtk+/3.16  gtk+-3.16.7  tar.xz  true
 
   # make all incl. tests and examples runs through fine
-  # make install fails with issue with 
-  # 
+  # make install fails with issue with
+  #
   # make[5]: Entering directory '/home/soegtrop/GTK/gtk+-3.16.7/demos/gtk-demo'
   # test -n "" || ../../gtk/gtk-update-icon-cache --ignore-theme-index --force "/usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor"
   # gtk-update-icon-cache.exe: Failed to open file /usr/x86_64-w64-mingw32/sys-root/mingw/share/icons/hicolor/.icon-theme.cache : No such file or directory
@@ -676,7 +678,8 @@ function make_libxml2 {
   if build_prep https://git.gnome.org/browse/libxml2/snapshot  libxml2-2.9.1  tar.xz ; then
     # ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --disable-shared --without-python
     # shared library required by gtksourceview
-    ./autogen.sh --build=$BUILD --host=$HOST --target=$TARGET --prefix="$PREFIX" --without-python
+    ./autogen.sh --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIX" --without-python
+    # shellcheck disable=SC2086
     log1 make $MAKE_OPT all
     log2 make install
     log2 make clean
@@ -708,12 +711,12 @@ function make_gtk_sourceview2 {
 # Install flexdll objects
 
 function install_flexdll {
-  cp flexdll.h /usr/$TARGET_ARCH/sys-root/mingw/include
+  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 "/usr/$TARGET_ARCH/bin"
     cp flexdll*_mingw.o "$PREFIXOCAML/bin"
   elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
-    cp flexdll*_mingw64.o /usr/$TARGET_ARCH/bin
+    cp flexdll*_mingw64.o "/usr/$TARGET_ARCH/bin"
     cp flexdll*_mingw64.o "$PREFIXOCAML/bin"
   else
     echo "Unknown target architecture"
@@ -724,8 +727,8 @@ function install_flexdll {
 # Install flexlink
 
 function install_flexlink {
-  cp flexlink.exe /usr/$TARGET_ARCH/bin
-    
+  cp flexlink.exe "/usr/$TARGET_ARCH/bin"
+
   cp flexlink.exe "$PREFIXOCAML/bin"
 }
 
@@ -745,8 +748,10 @@ function get_flex_dll_link_bin {
 function make_flex_dll_link {
   if build_prep http://alain.frisch.fr/flexdll flexdll-0.34 tar.gz ; then
     if [ "$TARGET_ARCH" == "i686-w64-mingw32" ]; then
+      # shellcheck disable=SC2086
       log1 make $MAKE_OPT build_mingw flexlink.exe
     elif [ "$TARGET_ARCH" == "x86_64-w64-mingw32" ]; then
+      # shellcheck disable=SC2086
       log1 make $MAKE_OPT build_mingw64 flexlink.exe
     else
       echo "Unknown target architecture"
@@ -769,11 +774,11 @@ function make_ln {
   if [ ! -f flagfiles/myln.finished ] ; then
     touch flagfiles/myln.started
     mkdir -p myln
-    cd myln
+    ( cd myln
     cp $PATCHES/ln.c .
-    $TARGET_ARCH-gcc -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c 
+    "$TARGET_ARCH-gcc" -DUNICODE -D_UNICODE -DIGNORE_SYMBOLIC -mconsole -o ln.exe ln.c
     install -D ln.exe "$PREFIXCOQ/bin/ln.exe"
-    cd ..
+    )
     touch flagfiles/myln.finished
   fi
 }
@@ -799,14 +804,14 @@ function make_ocaml {
     # 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 directory structure so put the OCaml library in a separate folder
     # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path:
     # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml
     # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4
     # So we put an explicit path in there
     sed -i "s|^LIBDIR=.*|LIBDIR=$PREFIXOCAML/libocaml|" config/Makefile
-    
+
     # Note: ocaml doesn't support -j 8, so don't pass MAKE_OPT
     # I verified that 4.02.3 still doesn't support parallel build
     log2 make world -f Makefile.nt
@@ -815,12 +820,12 @@ function make_ocaml {
     log2 make opt.opt -f Makefile.nt
     log2 make install -f Makefile.nt
     # TODO log2 make clean -f Makefile.nt Temporarily disabled for ocamlbuild development
-    
+
     # Move license files and other into into special folder
     if [ "$INSTALLMODE" == "absolute" ] || [ "$INSTALLMODE" == "relocatable" ]; then
       mkdir -p "$PREFIXOCAML/license_readme/ocaml"
       # 4.01 installs these files, 4.02 doesn't. So delete them and copy them from the sources.
-      rm -f *.txt
+      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"
@@ -909,9 +914,10 @@ function make_camlp5 {
   make_ocaml
   make_findlib
   if build_prep http://camlp5.gforge.inria.fr/distrib/src camlp5-6.14 tgz 1 ; then
-    logn configure ./configure 
+    logn configure ./configure
     # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
     sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
+    # shellcheck disable=SC2086
     log1 make world.opt $MAKE_OPT
     log2 make install
     # For some reason gramlib.a is not copied, but it is required by Coq
@@ -939,15 +945,15 @@ function make_lablgtk {
   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"
-    
+    cp "/bin/$TARGET_ARCH-pkg-config.exe"  bin_special/pkg-config.exe
+    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" --prefix="$PREFIXOCAML"
+
     # lablgtk shows occasional errors with -j, so don't pass $MAKE_OPT
-    
+
     # See https://sympa.inria.fr/sympa/arc/caml-list/2015-10/msg00204.html for the make || true + strip
     logn make-world-pre make world || true
-    $TARGET_ARCH-strip.exe --strip-unneeded src/dlllablgtk2.dll
-    
+    "$TARGET_ARCH-strip.exe" --strip-unneeded src/dlllablgtk2.dll
+
     log2 make world
     log2 make install
     log2 make clean
@@ -978,7 +984,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
 }
 
@@ -994,7 +1000,7 @@ function copy_coq_dlls {
   # Do this recursively until there are no further missing DLLs (File close + reopen)
   # For running this quickly, just do "cd coq-<ver> ; call copy_coq_dlls ; cd .." at the end of this script.
   # Do the same for coqc and ocamlc (usually doesn't result in additional files)
-  
+
   copy_coq_dll LIBATK-1.0-0.DLL
   copy_coq_dll LIBCAIRO-2.DLL
   copy_coq_dll LIBEXPAT-1.DLL
@@ -1018,7 +1024,7 @@ function copy_coq_dlls {
   copy_coq_dll LIBXML2-2.DLL
   copy_coq_dll ZLIB1.DLL
 
-  # Depends on if GTK is built from sources  
+  # Depends on if GTK is built from sources
   if [ "$GTK_FROM_SOURCES" == "Y" ]; then
     copy_coq_dll libiconv-2.dll
   else
@@ -1036,21 +1042,21 @@ function copy_coq_dlls {
     i686)   copy_coq_dll LIBGCC_S_SJLJ-1.DLL ;;
     *)      false ;;
   esac
-  
+
   # Win pthread version change
   copy_coq_dll LIBWINPTHREAD-1.DLL
 }
 
 function copy_coq_objects {
   # copy objects only from folders which exist in the target lib directory
-  find . -type d | while read FOLDER ; do
+  find . -type d | while read -r 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" 
+      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
 }
@@ -1066,7 +1072,7 @@ function copq_coq_gtk {
     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 [ -d "$PREFIXCOQ/share/coq/" ] ; then
       COQSHARE="$PREFIXCOQ/share/coq/"
@@ -1111,11 +1117,11 @@ function make_coq {
     case $COQ_VERSION in
       # 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-*) 
+      git-*)
         COQ_BUILD_PATH=/build/coq-${COQ_VERSION}
-        build_prep https://github.com/coq/coq/archive ${COQ_VERSION##git-} zip 1 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
@@ -1124,11 +1130,11 @@ function make_coq {
         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
+        build_prep "https://coq.inria.fr/distrib/V$COQ_VERSION/files" "coq-$COQ_VERSION" tar.gz
         ;;
     esac
   then
@@ -1142,16 +1148,17 @@ function make_coq {
     fi
 
     # The windows resource compiler binary name is hard coded
-    sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build 
+    sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.build
     sed -i "s/i686-w64-mingw32-windres/$TARGET_ARCH-windres/" Makefile.ide || true
 
     # 8.4x doesn't support parallel make
     if [[ $COQ_VERSION == 8.4* ]] ; then
       log1 make
     else
+      # shellcheck disable=SC2086
       make $MAKE_OPT
     fi
-    
+
     if [ "$INSTALLMODE" == "relocatable" ]; then
       ./configure -with-doc no -prefix "$PREFIXCOQ" -libdir "$PREFIXCOQ/lib" -mandir "$PREFIXCOQ/man"
     fi
@@ -1161,7 +1168,7 @@ function make_coq {
     if [ "$INSTALLOCAML" == "Y" ]; then
       copy_coq_objects
     fi
-    
+
     copq_coq_gtk
     copy_coq_license
 
@@ -1169,7 +1176,7 @@ function make_coq {
     # 1.) find | xargs fails on cygwin, can be fixed by sed -i 's|\| xargs rm -f|-exec rm -fv \{\} \+|' Makefile
     # 2.) clean of test suites fails with "cannot run complexity tests (no bogomips found)"
     # make clean
-    
+
     build_post
   fi
 }
@@ -1180,7 +1187,7 @@ function make_mingw_make {
   if build_prep http://ftp.gnu.org/gnu/make make-4.2 tar.bz2 ; then
     # The config.h.win32 file is fine - don't edit it
     # We need to copy the mingw gcc here as "gcc" - then the batch file will use it
-    cp /usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe ./gcc.exe
+    cp "/usr/bin/${ARCH}-w64-mingw32-gcc-6.4.0.exe" ./gcc.exe
     # By some magic cygwin bash can run batch files
     logn build ./build_w32.bat gcc
     # Copy make to Coq folder
@@ -1193,7 +1200,8 @@ 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-"
+    # shellcheck disable=SC2086
     log1 make $MAKE_OPT
     log2 make install
     # log2 make clean
@@ -1219,12 +1227,13 @@ function make_gcc {
     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" \
+    logn configure ./configure --build="$BUILD" --host="$HOST" --target="$TARGET" \
+        --prefix="$PREFIXCOQ" --program-prefix="$TARGET-" --disable-win32-registry --with-sysroot="$PREFIXCOQ" \
         --enable-languages=c --disable-nls \
         --disable-libsanitizer --disable-libssp --disable-libquadmath --disable-libgomp --disable-libvtv --disable-lto
         # --disable-decimal-float seems to be required
         # --with-sysroot="$PREFIX"  results in configure error that this is not an absolute path
+    # shellcheck disable=SC2086
     log1 make $MAKE_OPT
     log2 make install
     # log2 make clean
@@ -1252,21 +1261,22 @@ function get_cygwin_mingw_sources {
     # Take the 2nd field of the last line          => ${SOURCE} = x86_64/release/mingw64-x86_64-gcc/mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
     # Remove that path part                        => ${SOURCEFILE} = mingw64-x86_64-gcc-5.4.0-2-src.tar.xz
 
-    grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//'  | while read ARCHIVE ; do
+    grep "mingw" /etc/setup/installed.db | sed 's/\.tar\.bz2 [0-1]$//' | sed 's/ /\//'  | while read -r ARCHIVE ; do
       local ARCHIVEESC=${ARCHIVE//+/\\+}
-      local SOURCE=`egrep -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2`
+      local SOURCE
+      SOURCE=$(grep -E -A 1 "install: ($CYGWINARCH|noarch)/release/[-+_/a-z0-9]*$ARCHIVEESC" $TARBALLS/setup.ini | tail -1 | cut -d " " -f 2)
       local SOURCEFILE=${SOURCE##*/}
 
       # Get the source file (either from the source cache or online)
-      if [ ! -f $TARBALLS/$SOURCEFILE ] ; then
+      if [ ! -f "$TARBALLS/$SOURCEFILE" ] ; then
         if [ -f "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" ] ; then
           cp "$SOURCE_LOCAL_CACHE_CFMT/$SOURCEFILE" $TARBALLS
         else
           wget "$CYGWIN_REPOSITORY/$SOURCE"
-          mv $SOURCEFILE $TARBALLS
+          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"
+            cp "$TARBALLS/$SOURCEFILE" "$SOURCE_LOCAL_CACHE_CFMT"
           fi
         fi
       fi
@@ -1288,19 +1298,19 @@ function make_coq_installer {
   # ocaml: ocaml + menhir + camlp5 + findlib
   # ocaml_coq: as above + coq
   # ocaml_coq_addons: as above + lib/user-contrib/*
-  
+
   # Create coq file list as ocaml_coq / ocaml
   diff_files coq ocaml_coq ocaml
-  
+
   # Filter out object files
-  filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$' 
-  
+  filter_files coq_objects coq '\.(cmxa|cmi|cma|cmo|a|o)$'
+
   # Filter out plugin object files
   filter_files coq_objects_plugins coq_objects '/lib/plugins/.*\.(cmxa|cmi|cma|cmo|a|o)$'
-  
+
   # Coq objects objects required for plugin development = coq objects except those for pre installed plugins
   diff_files coq_plugindev coq_objects coq_objects_plugins
-  
+
   # Addons (TODO: including objects that could go to the plugindev thing, but
   # then one would have to make that package depend on this one, so not
   # implemented yet)
@@ -1308,27 +1318,27 @@ function make_coq_installer {
 
   # Coq files, except objects needed only for plugin development
   diff_files coq_base coq coq_plugindev
-  
+
   # Convert section files to NSIS format
   files_to_nsis coq_base
   files_to_nsis coq_addons
   files_to_nsis coq_plugindev
   files_to_nsis ocaml
-  
+
   # Get and extract NSIS Binaries
   if build_prep http://downloads.sourceforge.net/project/nsis/NSIS%202/2.51 nsis-2.51 zip ; then
-    NSIS=`pwd`/makensis.exe
+    NSIS=$(pwd)/makensis.exe
     chmod u+x "$NSIS"
     # Change to Coq folder
-    cd $COQ_BUILD_PATH
+    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 | tr -d '\r'`
+    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 -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
-    
+    logn nsis-installer "$NSIS" -DVERSION="$VERSION" -DARCH="$ARCH" -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi
+
     build_post
   fi
 }
@@ -1346,7 +1356,7 @@ function make_addon_bignums {
 
 function make_addons {
   for addon in $COQ_ADDONS; do
-    make_addon_$addon
+    "make_addon_$addon"
   done
 }
 
@@ -1374,4 +1384,3 @@ list_files ocaml_coq_addons
 if [ "$MAKEINSTALLER" == "Y" ] ; then
   make_coq_installer
 fi
-
diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh
index 524a55a42..93e7bd99a 100644
--- a/dev/ci/appveyor.sh
+++ b/dev/ci/appveyor.sh
@@ -4,6 +4,6 @@ wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/o
 tar -xf opam64.tar.xz
 bash opam64/install.sh
 opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c
-eval $(opam config env)
+eval "$(opam config env)"
 opam install -y ocamlfind camlp5
-cd $APPVEYOR_BUILD_FOLDER && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
+cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index c90e516ae..008291967 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -6,11 +6,11 @@ ci_dir="$(dirname "$0")"
 # Let's avoid to source ci-common twice in this case
 if [ -z "${CI_BUILD_DIR}" ];
 then
-    source ${ci_dir}/ci-common.sh
+    . "${ci_dir}/ci-common.sh"
 fi
 
-bignums_CI_DIR=${CI_BUILD_DIR}/Bignums
+bignums_CI_DIR="${CI_BUILD_DIR}/Bignums"
 
-git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR}
+git_checkout "${bignums_CI_BRANCH}" "${bignums_CI_GITURL}" "${bignums_CI_DIR}"
 
-( cd ${bignums_CI_DIR} && make && make install)
+( cd "${bignums_CI_DIR}" && make && make install)
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 558e8cbb8..8ce5f2418 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
 CoLoR_CI_DIR=${CI_BUILD_DIR}/color
 
 # Compile CoLoR
-git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR}
-( cd ${CoLoR_CI_DIR} && make )
+git_checkout "${CoLoR_CI_BRANCH}" "${CoLoR_CI_GITURL}" "${CoLoR_CI_DIR}"
+( cd "${CoLoR_CI_DIR}" && make )
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index d7a356930..189734a0b 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -20,7 +20,8 @@ else
         export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
         export CI_BRANCH="$CIRCLE_BRANCH"
     else # assume local
-        export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
+        CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
+        export CI_BRANCH
     fi
     export COQBIN="$PWD/bin"
 fi
@@ -35,10 +36,10 @@ ls "$COQBIN"
 CI_BUILD_DIR="$PWD/_build_ci"
 
 # shellcheck source=ci-basic-overlay.sh
-source "${ci_dir}/ci-basic-overlay.sh"
+. "${ci_dir}/ci-basic-overlay.sh"
 for overlay in "${ci_dir}"/user-overlays/*.sh; do
     # shellcheck source=/dev/null
-    source "${overlay}"
+    . "${overlay}"
 done
 
 mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
@@ -68,7 +69,7 @@ git_checkout()
 
 checkout_mathcomp()
 {
-  git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1}
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}"
 }
 
 make()
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 6a0ce2aef..fbdeff20c 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -1,11 +1,11 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
+CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert"
 
 opam install -j "$NJOBS" -y menhir
-git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
+git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}"
 
-( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
+( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh
index 5d6bd6a36..5d57fce1c 100755
--- a/dev/ci/ci-coq-dpdgraph.sh
+++ b/dev/ci/ci-coq-dpdgraph.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph
+coq_dpdgraph_CI_DIR="${CI_BUILD_DIR}/coq-dpdgraph"
 
-git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR}
+git_checkout "${coq_dpdgraph_CI_BRANCH}" "${coq_dpdgraph_CI_GITURL}" "${coq_dpdgraph_CI_DIR}"
 
-( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make && make test-suite )
+( cd "${coq_dpdgraph_CI_DIR}" && autoconf && ./configure && make && make test-suite )
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index 40eff03b7..d86d61ef6 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -1,12 +1,12 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-Coquelicot_CI_DIR=${CI_BUILD_DIR}/coquelicot
+Coquelicot_CI_DIR="${CI_BUILD_DIR}/coquelicot"
 
 install_ssreflect
 
-git_checkout ${Coquelicot_CI_BRANCH} ${Coquelicot_CI_GITURL} ${Coquelicot_CI_DIR}
+git_checkout "${Coquelicot_CI_BRANCH}" "${Coquelicot_CI_GITURL}" "${Coquelicot_CI_DIR}"
 
-( cd ${Coquelicot_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+( cd "${Coquelicot_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
index 54cad5df4..9298fc70a 100755
--- a/dev/ci/ci-corn.sh
+++ b/dev/ci/ci-corn.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-Corn_CI_DIR=${CI_BUILD_DIR}/corn
+Corn_CI_DIR="${CI_BUILD_DIR}/corn"
 
-git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
+git_checkout "${Corn_CI_BRANCH}" "${Corn_CI_GITURL}" "${Corn_CI_DIR}"
 
-( cd ${Corn_CI_DIR} && make && make install )
+( cd "${Corn_CI_DIR}" && make && make install )
diff --git a/dev/ci/ci-cpdt.sh b/dev/ci/ci-cpdt.sh
index 8b725f6fe..ca759c7b3 100755
--- a/dev/ci/ci-cpdt.sh
+++ b/dev/ci/ci-cpdt.sh
@@ -1,10 +1,9 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
 wget http://adam.chlipala.net/cpdt/cpdt.tgz
 tar xvfz cpdt.tgz
 
 ( cd cpdt && make clean && make )
-
diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh
index c44e0a655..9c58034be 100755
--- a/dev/ci/ci-elpi.sh
+++ b/dev/ci/ci-elpi.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-Elpi_CI_DIR=${CI_BUILD_DIR}/elpi
+Elpi_CI_DIR="${CI_BUILD_DIR}/elpi"
 
-git_checkout ${Elpi_CI_BRANCH} ${Elpi_CI_GITURL} ${Elpi_CI_DIR}
+git_checkout "${Elpi_CI_BRANCH}" "${Elpi_CI_GITURL}" "${Elpi_CI_DIR}"
 
-( cd ${Elpi_CI_DIR} && make && make install )
+( cd "${Elpi_CI_DIR}" && make && make install )
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 62854afac..98735b4ec 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-Equations_CI_DIR=${CI_BUILD_DIR}/Equations
+Equations_CI_DIR="${CI_BUILD_DIR}/Equations"
 
-git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR}
+git_checkout "${Equations_CI_BRANCH}" "${Equations_CI_GITURL}" "${Equations_CI_DIR}"
 
-( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install)
+( cd "${Equations_CI_DIR}" && coq_makefile -f _CoqProject -o Makefile && make && make test-suite && make examples && make install)
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh
index 5ca3ac47f..6c8dce5bd 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat-crypto.sh
@@ -1,11 +1,11 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-fiat_crypto_CI_DIR=${CI_BUILD_DIR}/fiat-crypto
+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 )
+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 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 292331b81..35c228405 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat-parsers.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-fiat_parsers_CI_DIR=${CI_BUILD_DIR}/fiat
+fiat_parsers_CI_DIR="${CI_BUILD_DIR}/fiat"
 
-git_checkout ${fiat_parsers_CI_BRANCH} ${fiat_parsers_CI_GITURL} ${fiat_parsers_CI_DIR}
+git_checkout "${fiat_parsers_CI_BRANCH}" "${fiat_parsers_CI_GITURL}" "${fiat_parsers_CI_DIR}"
 
-( cd ${fiat_parsers_CI_DIR} && make parsers parsers-examples && make fiat-core )
+( cd "${fiat_parsers_CI_DIR}" && make parsers parsers-examples && make fiat-core )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index ec19bd993..8599e4d50 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-Flocq_CI_DIR=${CI_BUILD_DIR}/flocq
+Flocq_CI_DIR="${CI_BUILD_DIR}/flocq"
 
-git_checkout ${Flocq_CI_BRANCH} ${Flocq_CI_GITURL} ${Flocq_CI_DIR}
+git_checkout "${Flocq_CI_BRANCH}" "${Flocq_CI_GITURL}" "${Flocq_CI_DIR}"
 
-( cd ${Flocq_CI_DIR} && ./autogen.sh && ./configure && ./remake -j${NJOBS} )
+( cd "${Flocq_CI_DIR}" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 53eb55fc4..118d15150 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
+formal_topology_CI_DIR="${CI_BUILD_DIR}/formal-topology"
 
-git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR}
+git_checkout "${formal_topology_CI_BRANCH}" "${formal_topology_CI_GITURL}" "${formal_topology_CI_DIR}"
 
-( cd ${formal_topology_CI_DIR} && make )
+( cd "${formal_topology_CI_DIR}" && make )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 8e6448e76..bd1d88993 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -1,12 +1,12 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-GeoCoq_CI_DIR=${CI_BUILD_DIR}/GeoCoq
+GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq"
 
-git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} ${GeoCoq_CI_DIR}
+git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}"
 
-( cd ${GeoCoq_CI_DIR}                                     && \
+( cd "${GeoCoq_CI_DIR}"                                     && \
   ./configure-ci.sh                                       && \
   make )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 693135a4c..6ded97984 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT
+HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT
 
-git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR}
+git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}"
 
-( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make )
+( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index 267e13359..b019fa059 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -1,11 +1,11 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-stdpp_CI_DIR=${CI_BUILD_DIR}/coq-stdpp
-Iris_CI_DIR=${CI_BUILD_DIR}/iris-coq
-lambdaRust_CI_DIR=${CI_BUILD_DIR}/lambdaRust
+stdpp_CI_DIR="${CI_BUILD_DIR}/coq-stdpp"
+Iris_CI_DIR="${CI_BUILD_DIR}/iris-coq"
+lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust"
 
 install_ssreflect
 
@@ -13,29 +13,29 @@ install_ssreflect
 opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev
 
 # Setup lambdaRust first
-git_checkout ${lambdaRust_CI_BRANCH} ${lambdaRust_CI_GITURL} ${lambdaRust_CI_DIR}
+git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}"
 
 # Extract required version of Iris
-Iris_VERSION=$(cat ${lambdaRust_CI_DIR}/opam | fgrep coq-iris | egrep 'dev\.([0-9.-]+)' -o)
-Iris_URL=$(opam show coq-iris.$Iris_VERSION -f upstream-url)
-read -a Iris_URL_PARTS <<< $(echo $Iris_URL | tr '#' ' ')
+Iris_VERSION=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o)
+Iris_URL=$(opam show "coq-iris.$Iris_VERSION" -f upstream-url)
+read -r -a Iris_URL_PARTS <<< "$(echo "$Iris_URL" | tr '#' ' ')"
 
 # Setup Iris
-git_checkout ${Iris_CI_BRANCH} ${Iris_URL_PARTS[0]} ${Iris_CI_DIR} ${Iris_URL_PARTS[1]}
+git_checkout "${Iris_CI_BRANCH}" "${Iris_URL_PARTS[0]}" "${Iris_CI_DIR}" "${Iris_URL_PARTS[1]}"
 
 # Extract required version of std++
-stdpp_VERSION=$(cat ${Iris_CI_DIR}/opam | fgrep coq-stdpp | egrep 'dev\.([0-9.-]+)' -o)
-stdpp_URL=$(opam show coq-stdpp.$stdpp_VERSION -f upstream-url)
-read -a stdpp_URL_PARTS <<< $(echo $stdpp_URL | tr '#' ' ')
+stdpp_VERSION=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o)
+stdpp_URL=$(opam show "coq-stdpp.$stdpp_VERSION" -f upstream-url)
+read -r -a stdpp_URL_PARTS <<< "$(echo "$stdpp_URL" | tr '#' ' ')"
 
 # Setup std++
-git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]}
+git_checkout "${stdpp_CI_BRANCH}" "${stdpp_URL_PARTS[0]}" "${stdpp_CI_DIR}" "${stdpp_URL_PARTS[1]}"
 
 # Build std++
-( cd ${stdpp_CI_DIR} && make && make install )
+( cd "${stdpp_CI_DIR}" && make && make install )
 
 # Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris
-( cd ${Iris_CI_DIR} && make && (test -n "${TRAVIS}" || make validate) && make install )
+( cd "${Iris_CI_DIR}" && make && (test -n "${TRAVIS}" || make validate) && make install )
 
 # Build lambdaRust
-( cd ${lambdaRust_CI_DIR} && make && make install )
+( cd "${lambdaRust_CI_DIR}" && make && make install )
diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh
index 820ff89ee..5981aaaae 100755
--- a/dev/ci/ci-ltac2.sh
+++ b/dev/ci/ci-ltac2.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2
+ltac2_CI_DIR="${CI_BUILD_DIR}/ltac2"
 
-git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR}
+git_checkout "${ltac2_CI_BRANCH}" "${ltac2_CI_GITURL}" "${ltac2_CI_DIR}"
 
-( cd ${ltac2_CI_DIR} && make && make tests && make install )
+( cd "${ltac2_CI_DIR}" && make && make tests && make install )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index db4a31e54..4fc06e895 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
+math_classes_CI_DIR="${CI_BUILD_DIR}/math-classes"
 
-git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
+git_checkout "${math_classes_CI_BRANCH}" "${math_classes_CI_GITURL}" "${math_classes_CI_DIR}"
 
-( cd ${math_classes_CI_DIR} && make && make install )
+( cd "${math_classes_CI_DIR}" && make && make install )
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh
index 701403f2c..8c6b910bb 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-math-comp.sh
@@ -2,14 +2,14 @@
 
 # $0 is not the safest way, but...
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp
+mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp"
 
-checkout_mathcomp ${mathcomp_CI_DIR}
+checkout_mathcomp "${mathcomp_CI_DIR}"
 
 # odd_order takes too much time for travis.
-( cd ${mathcomp_CI_DIR}/mathcomp                  && \
+( 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 all )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
index c813b1fe9..a66dc1e76 100755
--- a/dev/ci/ci-metacoq.sh
+++ b/dev/ci/ci-metacoq.sh
@@ -1,19 +1,19 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
 unicoq_CI_DIR=${CI_BUILD_DIR}/unicoq
 metacoq_CI_DIR=${CI_BUILD_DIR}/MetaCoq
 
 # Setup UniCoq
 
-git_checkout ${unicoq_CI_BRANCH} ${unicoq_CI_GITURL} ${unicoq_CI_DIR}
+git_checkout "${unicoq_CI_BRANCH}" "${unicoq_CI_GITURL}" "${unicoq_CI_DIR}"
 
-( cd ${unicoq_CI_DIR} && coq_makefile -f Make -o Makefile && make && 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}
+git_checkout "${metacoq_CI_BRANCH}" "${metacoq_CI_GITURL}" "${metacoq_CI_DIR}"
 
-( cd ${metacoq_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make )
+( 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 4f7e9517f..58bbb7229 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -1,12 +1,12 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR}
-wget -qO- ${sf_lf_CI_TARURL}  | tar xvz
-wget -qO- ${sf_plf_CI_TARURL} | tar xvz
-wget -qO- ${sf_vfa_CI_TARURL} | tar xvz
+mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}" || exit 1
+wget -qO- "${sf_lf_CI_TARURL}"  | tar xvz
+wget -qO- "${sf_plf_CI_TARURL}" | tar xvz
+wget -qO- "${sf_vfa_CI_TARURL}" | tar xvz
 
 sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v
 sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v
diff --git a/dev/ci/ci-template.sh b/dev/ci/ci-template.sh
index 25da01a82..e77a55304 100755
--- a/dev/ci/ci-template.sh
+++ b/dev/ci/ci-template.sh
@@ -1,12 +1,12 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
 Template_CI_BRANCH=master
 Template_CI_GITURL=https://github.com/Template/Template
-Template_CI_DIR=${CI_BUILD_DIR}/Template
+Template_CI_DIR="${CI_BUILD_DIR}/Template"
 
-git_checkout ${Template_CI_BRANCH} ${Template_CI_GITURL} ${Template_CI_DIR}
+git_checkout "${Template_CI_BRANCH}" "${Template_CI_GITURL}" "${Template_CI_DIR}"
 
-( cd ${Template_CI_DIR} && make )
+( cd "${Template_CI_DIR}" && make )
diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh
index 8ecd8c441..31387c8dd 100755
--- a/dev/ci/ci-tlc.sh
+++ b/dev/ci/ci-tlc.sh
@@ -1,10 +1,10 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-tlc_CI_DIR=${CI_BUILD_DIR}/tlc
+tlc_CI_DIR="${CI_BUILD_DIR}/tlc"
 
-git_checkout ${tlc_CI_BRANCH} ${tlc_CI_GITURL} ${tlc_CI_DIR}
+git_checkout "${tlc_CI_BRANCH}" "${tlc_CI_GITURL}" "${tlc_CI_DIR}"
 
-( cd ${tlc_CI_DIR} && make )
+( cd "${tlc_CI_DIR}" && make )
diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh
index 66b56add7..62a949f59 100755
--- a/dev/ci/ci-unimath.sh
+++ b/dev/ci/ci-unimath.sh
@@ -1,14 +1,13 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-UniMath_CI_DIR=${CI_BUILD_DIR}/UniMath
+UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath"
 
-git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} ${UniMath_CI_DIR}
+git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}"
 
-( cd ${UniMath_CI_DIR}                        && \
+( cd "${UniMath_CI_DIR}"                        && \
   sed -i.bak '/Folds/d'              Makefile && \
   sed -i.bak '/HomologicalAlgebra/d' Makefile && \
   make BUILD_COQ=no )
-
diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh
index 5760fbafb..3c0044bfe 100755
--- a/dev/ci/ci-vst.sh
+++ b/dev/ci/ci-vst.sh
@@ -1,13 +1,13 @@
 #!/usr/bin/env bash
 
 ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
+. "${ci_dir}/ci-common.sh"
 
-VST_CI_DIR=${CI_BUILD_DIR}/VST
+VST_CI_DIR="${CI_BUILD_DIR}/VST"
 
 # opam install -j ${NJOBS} -y menhir
-git_checkout ${VST_CI_BRANCH} ${VST_CI_GITURL} ${VST_CI_DIR}
+git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}"
 
 # Targets are: msl veric floyd progs , we remove progs to save time
 # Patch to avoid the upper version limit
-( cd ${VST_CI_DIR} && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd )
+( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true .loadpath version.vo msl veric floyd )
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
index 7716bcb59..e9ba11414 100644
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -1,3 +1,5 @@
+#!/bin/sh
+
 if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
diff --git a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
deleted file mode 100644
index c2e367038..000000000
--- a/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then
-    Equations_CI_BRANCH=rm-local-polymorphic-flag
-    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh
deleted file mode 100644
index 78789a6fc..000000000
--- a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then
-    HoTT_CI_BRANCH=check-poly-effects
-    HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git
-fi
diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh
deleted file mode 100644
index 9677b3525..000000000
--- a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh
+++ /dev/null
@@ -1,8 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then
-    Equations_CI_BRANCH=API-removal
-    Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
-    coq_dpdgraph_CI_BRANCH=API-removal
-    coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git
-    ltac2_CI_BRANCH=API-removal
-    ltac2_CI_GITURL=https://github.com/gares/ltac2.git
-fi
diff --git a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh b/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
deleted file mode 100644
index 4b681909d..000000000
--- a/dev/ci/user-overlays/06511-ejgallego-econstr+more_fix.sh
+++ /dev/null
@@ -1,7 +0,0 @@
- if [ "$CI_PULL_REQUEST" = "6511" ] || [ "$CI_BRANCH" = "econstr+more_fix" ]; then
-    ltac2_CI_BRANCH=econstr+more_fix
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Equations_CI_BRANCH=econstr+more_fix
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh
deleted file mode 100644
index 8a50fb111..000000000
--- a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then
-    Equations_CI_BRANCH=fix-6535
-    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh b/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
deleted file mode 100644
index 2451657d4..000000000
--- a/dev/ci/user-overlays/06676-gares-proofview-goals-come-with-a-state.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6676" ] || [ "$CI_BRANCH" = "proofview/goal-w-state" ]; then
-    ltac2_CI_BRANCH=fix-for/6676
-    ltac2_CI_GITURL=https://github.com/gares/ltac2.git
-    Equations_CI_BRANCH=fix-for/6676
-    Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
-fi
diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh
deleted file mode 100644
index 3a3ab44e0..000000000
--- a/dev/ci/user-overlays/06686-ccnv-no-proj.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then
-    Equations_CI_BRANCH=ccnv-fixes
-    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
deleted file mode 100644
index d1d61fec2..000000000
--- a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then
-    ltac2_CI_BRANCH=located+vernac
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Equations_CI_BRANCH=located+vernac
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    fiat_parsers_CI_BRANCH=located+vernac
-    fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
-
-    Elpi_CI_BRANCH=located+vernac
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
-fi
diff --git a/dev/ci/user-overlays/06775-univ-cumul-weak.sh b/dev/ci/user-overlays/06775-univ-cumul-weak.sh
deleted file mode 100644
index 8afcbf78a..000000000
--- a/dev/ci/user-overlays/06775-univ-cumul-weak.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6775" ] || [ "$CI_BRANCH" = "univ-cumul" ]; then
-    Elpi_CI_BRANCH=coq-master
-    Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git
-fi
diff --git a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh b/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh
deleted file mode 100644
index df3e9cef2..000000000
--- a/dev/ci/user-overlays/06831-ejgallego-located+vernac_2.sh
+++ /dev/null
@@ -1,14 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6831" ] || [ "$CI_BRANCH" = "located+vernac_2" ]; then
-
-    ltac2_CI_BRANCH=located+vernac_2
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Equations_CI_BRANCH=located+vernac_2
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    # fiat_parsers_CI_BRANCH=located+vernac
-    # fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
-
-    Elpi_CI_BRANCH=located+vernac_2
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
-fi
diff --git a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh b/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh
deleted file mode 100644
index a785290e7..000000000
--- a/dev/ci/user-overlays/06837-ejgallego-located+libnames.sh
+++ /dev/null
@@ -1,15 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6837" ] || [ "$CI_BRANCH" = "located+libnames" ]; then
-
-    ltac2_CI_BRANCH=located+libnames
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Equations_CI_BRANCH=located+libnames
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    Elpi_CI_BRANCH=located+libnames
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
-
-    coq_dpdgraph_CI_BRANCH=located+libnames
-    coq_dpdgraph_CI_GITURL=https://github.com/ejgallego/coq-dpdgraph.git
-
-fi
diff --git a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh b/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
deleted file mode 100644
index 5dedca0ca..000000000
--- a/dev/ci/user-overlays/06869-ejgallego-ssr+correct_packing.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6869" ] || [ "$CI_BRANCH" = "ssr+correct_packing" ]; then
-
-    Equations_CI_BRANCH=ssr+correct_packing
-    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
-
-    ltac2_CI_BRANCH=ssr+correct_packing
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    Elpi_CI_BRANCH=ssr+correct_packing
-    Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git
-
-fi
diff --git a/dev/ci/user-overlays/06923-ppedrot-export-options.sh b/dev/ci/user-overlays/06923-ppedrot-export-options.sh
deleted file mode 100644
index 333a9e84b..000000000
--- a/dev/ci/user-overlays/06923-ppedrot-export-options.sh
+++ /dev/null
@@ -1,7 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6923" ] || [ "$CI_BRANCH" = "export-options" ]; then
-    ltac2_CI_BRANCH=export-options
-    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
-
-    Equations_CI_BRANCH=export-options
-    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
-fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 9f0377cee..a7474e324 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -7,6 +7,8 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
 ```
+#!/bin/sh
+
 if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index e4359f703..5205350a6 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -27,9 +27,9 @@ BRANCH=backport-pr-${PRNUM}
 RANGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%P" | sed 's/ /../')
 MESSAGE=$(git log master --grep "Merge PR #${PRNUM}" --format="%s" | sed 's/Merge/Backport/')
 
-if git checkout -b ${BRANCH}; then
+if git checkout -b "${BRANCH}"; then
 
-    if ! git cherry-pick -x ${RANGE}; then
+    if ! git cherry-pick -x "${RANGE}"; then
         echo "Please fix the conflicts, then exit."
         bash
         while ! git cherry-pick --continue; do
@@ -50,7 +50,7 @@ else
 
 fi
 
-if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+if ! git diff --exit-code HEAD "${BRANCH}" -- "*.mli"; then
     echo
     read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
     echo
@@ -63,8 +63,8 @@ if [[ "${OPTION}" == "--stop-before-merging" ]]; then
     exit 0
 fi
 
-git merge -S --no-ff ${BRANCH} -m "${MESSAGE}"
-git branch -d ${BRANCH}
+git merge -S --no-ff "${BRANCH}" -m "${MESSAGE}"
+git branch -d "${BRANCH}"
 
 # To-Do:
 # - Support for backporting a PR before it is merged
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index ecfdfab94..20612eeb8 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -80,8 +80,8 @@ if [ -z "$REMOTE" ]; then
   exit 1
 fi
 REMOTE_URL=$(git remote get-url "$REMOTE" --push)
-if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" -a \
-     "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
+if [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL" ] && \
+   [ "$REMOTE_URL" != "$OFFICIAL_REMOTE_URL.git" ]; then
   error "remote ${BLUE}$REMOTE${RESET} does not point to the official Coq repo"
   error "that is ${BLUE}$OFFICIAL_REMOTE_URL"
   error "it points to ${BLUE}$REMOTE_URL${RESET} instead"