Strip -no-native-compiler

It's not needed in Coq >= 8.5rc1 (or 8.5beta3?)

Makefile.am

@@ -185,7 +185,7 @@ checkproofs:
 
 $(STD_VOFILES) : %.vo : %.v coq-HoTT
 	$(VECHO) COQTOP $*
-	$(Q) $(TIMER) etc/pipe_out.sh "$*.timing" "$(COQTOP)" -time -indices-matter -boot -nois -no-native-compiler -coqlib "$(SRCCOQLIB)" -R "$(SRCCOQLIB)/theories" Coq -compile "$*"
+	$(Q) $(TIMER) etc/pipe_out.sh "$*.timing" "$(COQTOP)" -time -indices-matter -boot -nois -coqlib "$(SRCCOQLIB)" -R "$(SRCCOQLIB)/theories" Coq -compile "$*"
 
 
 # The HoTT library as a single target

coq/theories/.dir-locals.el

@@ -1,4 +1,4 @@
 ((coq-mode . ((eval . (let ((default-directory (locate-dominating-file
                                                 buffer-file-name ".dir-locals.el")))
                         (make-local-variable 'coq-prog-args)
-                        (setq coq-prog-args `("-no-native-compiler" "-indices-matter" "-boot" "-nois" "-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq" "-emacs")))))))
+                        (setq coq-prog-args `("-indices-matter" "-boot" "-nois" "-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq" "-emacs")))))))

etc/ci/install_coq.sh

@@ -37,8 +37,8 @@ if [ ! -z "$FORCE_COQ_VERSION" ]
 then
     git checkout "$FORCE_COQ_VERSION" || exit $?
 fi
-echo '$ ./configure -no-native-compiler '"$@"
-./configure -no-native-compiler "$@"
+echo '$ ./configure '"$@"
+./configure "$@"
 echo '$ make coqlight'
 make coqlight
 echo '$ sudo make install-coqlight install-devfiles'

etc/dpdgraph-0.4alpha/hoqthmdep

@@ -41,4 +41,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQTOP" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$mythmdepdir/coqthmdep" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$mythmdepdir/coqthmdep" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoq-config.in

@@ -49,4 +49,4 @@ else
   export HOTTLIB="@hottdir@/theories"
   export HOTTCONTRIB="@hottdir@/contrib"
 fi
-#export COQ_ARGS=(-no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter)
+#export COQ_ARGS=(-coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter)

hoqc

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQC" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQC" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQC" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoqdep

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQDEP" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQDEP" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQDEP" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoqide

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQIDE" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQIDE" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQIDE" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoqtop

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQTOP" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQTOP" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQTOP" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"

hoqtop.byte

@@ -46,4 +46,4 @@ fi
 # or using more evil (but portable) 'eval', do
 # $ eval 'exec "$COQTOP.byte" '"$COQ_ARGS"' "$@"'
 # Instead, we duplicate code, because it's simpler.
-exec "$COQTOP.byte" -no-native-compiler -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"
+exec "$COQTOP.byte" -coqlib "$COQLIB" -R "$HOTTLIB" HoTT -Q "$HOTTCONTRIB" "" -indices-matter "$@"