[extra-dev] Update mathcomp packages

Following the merge of math-comp/math-comp#1329
coq · Jan 26, 2025 · e39f1a9 · e39f1a9
1 parent 11175e8
commit e39f1a9
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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