From c35b6de2b912ea959f3f1837ee570a4dfc3d4616 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 29 Jul 2024 17:05:32 +0900 Subject: [PATCH] add Coq 8.20 --- coq-mathcomp-analysis.opam | 1 + coq-mathcomp-classical.opam | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index 99659934e..8fd87619e 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -18,6 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "theories" "-j%{jobs}%"] install: [make "-C" "theories" "install"] depends: [ + "coq" { (>= "8.18" & < "8.21~") | (= "dev") } "coq-mathcomp-classical" { = version} "coq-mathcomp-solvable" { (>= "2.0.0") | (= "dev") } "coq-mathcomp-field" diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index ec55f13a3..ee058ceca 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -18,7 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "classical" "-j%{jobs}%"] install: [make "-C" "classical" "install"] depends: [ - "coq" { (>= "8.18" & < "8.20~") | (= "dev") } + "coq" { (>= "8.18" & < "8.21~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "2.1.0") | (= "dev") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra"