@@ -530,14 +530,14 @@ missingtools=false
530530echo " Testing Coq... " | tr -d ' \n'
531531coq_ver=$( ${COQBIN} coqc -v 2> /dev/null | sed -n -e ' s/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p' )
532532case " $coq_ver " in
533- 8.7.0|8.7.1|8.7.2|8. 8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1)
533+ 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1)
534534 echo " version $coq_ver -- good!" ;;
535535 ?* )
536536 echo " version $coq_ver -- UNSUPPORTED"
537537 if $ignore_coq_version ; then
538538 echo " Warning: this version of Coq is unsupported, proceed at your own risks."
539539 else
540- echo " Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0, 8.7.2, 8.7.1, 8.7.0 "
540+ echo " Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0"
541541 missingtools=true
542542 fi ;;
543543 " " )
@@ -549,15 +549,10 @@ esac
549549echo " Testing OCaml... " | tr -d ' \n'
550550ocaml_ver=` ocamlopt -version 2> /dev/null`
551551case " $ocaml_ver " in
552- 4.00.* |4.01.* )
552+ 4.00.* |4.01.* | 4.02. * |4.03. * |4.04. * )
553553 echo " version $ocaml_ver -- UNSUPPORTED"
554- echo " Error: CompCert requires OCaml version 4.02 or later."
554+ echo " Error: CompCert requires OCaml version 4.05 or later."
555555 missingtools=true;;
556- 4.02.* |4.03.* |4.04.* )
557- echo " version $ocaml_ver -- good!"
558- echo " WARNING: some Intel processors of the Skylake and Kaby Lake generations"
559- echo " have a hardware bug that can be triggered by this version of OCaml."
560- echo " To avoid this risk, it is recommended to use OCaml 4.05 or later." ;;
561556 4.0* )
562557 echo " version $ocaml_ver -- good!" ;;
563558 ? .* )
0 commit comments