From e39f1a96bd8a3a91418bc39f6693ab7d415bb257 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 26 Jan 2025 14:42:49 +0100 Subject: [PATCH] [extra-dev] Update mathcomp packages Following the merge of https://github.com/math-comp/math-comp/pull/1329 --- .../coq-mathcomp-algebra/coq-mathcomp-algebra.dev/opam | 4 ++-- .../coq-mathcomp-character/coq-mathcomp-character.dev/opam | 4 ++-- .../packages/coq-mathcomp-field/coq-mathcomp-field.dev/opam | 4 ++-- .../coq-mathcomp-fingroup/coq-mathcomp-fingroup.dev/opam | 4 ++-- .../coq-mathcomp-solvable/coq-mathcomp-solvable.dev/opam | 4 ++-- .../coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam | 4 ++-- 6 files changed, 12 insertions(+), 12 deletions(-) diff --git a/extra-dev/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.dev/opam b/extra-dev/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.dev/opam index 1794fb65fc..cf80ce07bf 100644 --- a/extra-dev/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.dev/opam +++ b/extra-dev/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.dev/opam @@ -7,8 +7,8 @@ bug-reports: "https://github.com/math-comp/math-comp/issues" dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" -build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ] -install: [ make "-C" "mathcomp/algebra" "install" ] +build: [ make "-C" "algebra" "-j" "%{jobs}%" ] +install: [ make "-C" "algebra" "install" ] depends: [ "coq-mathcomp-fingroup" { = version } ] tags: [ "keyword:algebra" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.algebra" ] diff --git a/extra-dev/packages/coq-mathcomp-character/coq-mathcomp-character.dev/opam b/extra-dev/packages/coq-mathcomp-character/coq-mathcomp-character.dev/opam index 95465498e9..ba822de17a 100644 --- a/extra-dev/packages/coq-mathcomp-character/coq-mathcomp-character.dev/opam +++ b/extra-dev/packages/coq-mathcomp-character/coq-mathcomp-character.dev/opam @@ -7,8 +7,8 @@ bug-reports: "https://github.com/math-comp/math-comp/issues" dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" -build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" ] -install: [ make "-C" "mathcomp/character" "install" ] +build: [ make "-C" "character" "-j" "%{jobs}%" ] +install: [ make "-C" "character" "install" ] depends: [ "coq-mathcomp-field" { = version } ] tags: [ "keyword:algebra" "keyword:character" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.character" ] diff --git a/extra-dev/packages/coq-mathcomp-field/coq-mathcomp-field.dev/opam b/extra-dev/packages/coq-mathcomp-field/coq-mathcomp-field.dev/opam index 45374e83ef..9c741d0d7c 100644 --- a/extra-dev/packages/coq-mathcomp-field/coq-mathcomp-field.dev/opam +++ b/extra-dev/packages/coq-mathcomp-field/coq-mathcomp-field.dev/opam @@ -7,8 +7,8 @@ bug-reports: "https://github.com/math-comp/math-comp/issues" dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" -build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" ] -install: [ make "-C" "mathcomp/field" "install" ] +build: [ make "-C" "field" "-j" "%{jobs}%" ] +install: [ make "-C" "field" "install" ] depends: [ "coq-mathcomp-solvable" { = version } ] tags: [ "keyword:algebra" "keyword:field" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.field" ] diff --git a/extra-dev/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.dev/opam b/extra-dev/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.dev/opam index e1a8195d85..381f6def3c 100644 --- a/extra-dev/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.dev/opam +++ b/extra-dev/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.dev/opam @@ -7,8 +7,8 @@ bug-reports: "https://github.com/math-comp/math-comp/issues" dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" -build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" ] -install: [ make "-C" "mathcomp/fingroup" "install" ] +build: [ make "-C" "fingroup" "-j" "%{jobs}%" ] +install: [ make "-C" "fingroup" "install" ] depends: [ "coq-mathcomp-ssreflect" { = version } ] tags: [ "keyword:finite groups" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.fingroup" ] diff --git a/extra-dev/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.dev/opam b/extra-dev/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.dev/opam index b182a90e01..5616ef6919 100644 --- a/extra-dev/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.dev/opam +++ b/extra-dev/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.dev/opam @@ -7,8 +7,8 @@ bug-reports: "https://github.com/math-comp/math-comp/issues" dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" -build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" ] -install: [ make "-C" "mathcomp/solvable" "install" ] +build: [ make "-C" "solvable" "-j" "%{jobs}%" ] +install: [ make "-C" "solvable" "install" ] depends: [ "coq-mathcomp-algebra" { = version } ] tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.solvable" ] diff --git a/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam b/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam index 0f2c1bab66..b7735e0404 100644 --- a/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam +++ b/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam @@ -7,8 +7,8 @@ bug-reports: "https://github.com/math-comp/math-comp/issues" dev-repo: "git+https://github.com/math-comp/math-comp.git" license: "CeCILL-B" -build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ] -install: [ make "-C" "mathcomp/ssreflect" "install" ] +build: [ make "-C" "ssreflect" "-j" "%{jobs}%" ] +install: [ make "-C" "ssreflect" "install" ] depends: [ ( ( "coq" {>= "8.16" & < "8.17~"} & "elpi" {>= "1.16.5"} ) | # The line above can be removed at the time support for 8.16 is dropped