Blob Blame History Raw
--- why3-1.6.0/configure.in.orig	2023-03-07 02:15:31.000000000 -0700
+++ why3-1.6.0/configure.in	2023-06-26 14:21:56.361457115 -0600
@@ -993,6 +993,10 @@ if test "$enable_coq_support" = yes; the
       8.16*)
          coq_compat_version="COQ816"
          ;;
+      8.17*)
+         coq_compat_version="COQ817"
+         COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality"
+         ;;
       *)
          enable_coq_support=no
          AC_MSG_WARN([You need Coq 8.7 or later; Coq discarded.])
@@ -1242,6 +1246,7 @@ AC_SUBST(COQC)
 AC_SUBST(COQDEP)
 AC_SUBST(COQLIB)
 AC_SUBST(COQVERSION)
+AC_SUBST(COQFLAGS)
 
 AC_SUBST(enable_pvs_libs)
 AC_SUBST(PVS)
--- why3-1.6.0/configure.orig	2023-03-07 02:15:31.000000000 -0700
+++ why3-1.6.0/configure	2023-06-26 14:35:07.856280739 -0600
@@ -696,6 +696,7 @@ PVSVERSION
 enable_pvs_libs
 COQVERSION
 COQLIB
+COQFLAGS
 coq_compat_version
 enable_coq_fp_libs
 enable_coq_libs
@@ -5926,6 +5927,10 @@ printf "%s\n" "$COQVERSION" >&6; }
       8.16*)
          coq_compat_version="COQ816"
          ;;
+      8.17*)
+         coq_compat_version="COQ817"
+         COQFLAGS="-w deprecated-instance-without-locality,deprecated-hint-without-locality"
+         ;;
       *)
          enable_coq_support=no
          { printf "%s\n" "$as_me:${as_lineno-$LINENO}: WARNING: You need Coq 8.7 or later; Coq discarded." >&5
--- why3-1.6.0/Makefile.in.orig	2023-03-07 02:15:31.000000000 -0700
+++ why3-1.6.0/Makefile.in	2023-06-26 14:21:12.426061732 -0600
@@ -62,6 +62,7 @@ OCAMLBEST = @OCAMLBEST@
 OCAMLVERSION = @OCAMLVERSION@
 COQC      = @COQC@
 COQDEP    = @COQDEP@
+COQFLAGS  = @COQFLAGS@
 FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
 MENHIR	  = @MENHIR@
 
@@ -1068,7 +1069,7 @@ COQLIBS_FILES = lib/coq/BuiltIn lib/coq/
 
 %.vo: %.v
 	$(SHOW) 'Coqc     $<'
-	$(HIDE)$(COQC) -R lib/coq Why3 $<
+	$(HIDE)$(COQC) $(COQFLAGS) -R lib/coq Why3 $<
 
 %.vd: %.v
 	$(SHOW) 'Coqdep   $<'
--- why3-1.6.0/share/provers-detection-data.conf.orig	2023-03-07 02:15:31.000000000 -0700
+++ why3-1.6.0/share/provers-detection-data.conf	2023-06-26 14:22:52.768680868 -0600
@@ -838,16 +838,8 @@ support_library = "%l/coq/version"
 exec = "coqtop"
 version_switch = "-v"
 version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
-version_ok = "^8\.16\.[0-9]+$"
-version_ok = "^8\.15\.[0-9]+$"
-version_ok = "^8\.14\.[0-9]+$"
-version_ok = "^8\.13\.[0-9]+$"
-version_ok = "^8\.12\.[0-9]+$"
-version_ok = "^8\.11\.[0-9]+$"
-version_ok = "^8\.10\.[0-9]+$"
-version_ok = "^8\.9\.[0-9]+$"
-version_ok = "^8\.8\.[0-9]+$"
-version_ok = "^8\.7\.[0-9]+$"
+version_ok = "^8\.1[0-7]\.[0-9]+$"
+version_ok = "^8\.[7-9]\.[0-9]+$"
 version_old = "8.6.1"
 version_old = "8.6"
 version_old = "^8\.5pl[1-3]$"