Skip to content

Commit 6fc6afa

Browse files
CohenCyrilstrub
CohenCyril
authored and
strub
committed
mathcomp 1.7.0 -> 1.8.0 (#25)
1 parent 764a57f commit 6fc6afa

File tree

5 files changed

+29
-30
lines changed

5 files changed

+29
-30
lines changed

‎.travis.yml‎

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -14,14 +14,14 @@ env:
1414
- NJOBS="2"
1515
- CONTRIB_NAME="multinomials"
1616
matrix:
17-
- DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-8.7"
18-
- DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-8.8"
19-
- DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-8.9"
20-
- DOCKERIMAGE="mathcomp/mathcomp:1.7.0-coq-dev"
21-
# - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.7"
22-
# - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.8"
23-
# - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.9"
24-
# - DOCKERIMAGE="mathcomp/mathcomp-dev:coq-dev"
17+
- DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.7"
18+
- DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.8"
19+
- DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.9"
20+
- DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-dev"
21+
- DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.7"
22+
- DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.8"
23+
- DOCKERIMAGE="mathcomp/mathcomp-dev:coq-8.9"
24+
- DOCKERIMAGE="mathcomp/mathcomp-dev:coq-dev"
2525

2626
install: |
2727
# Prepare the COQ container

‎descr‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎opam‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
opam-version: "1.2"
1+
opam-version: "2.0"
22
name: "coq-mathcomp-multinomials"
33
maintainer: "[email protected]"
44
homepage: "https://github.com/math-comp/multinomials-ssr"
@@ -15,11 +15,10 @@ install: [
1515
]
1616
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/SsrMultinomials"]
1717
depends: [
18-
"coq" {(>= "8.5" | = "dev")}
19-
"coq-mathcomp-ssreflect" { (>= "1.6" | = "dev") }
20-
"coq-mathcomp-algebra" { (>= "1.6" | = "dev") }
18+
"coq" {(>= "8.7" | = "dev")}
19+
"coq-mathcomp-algebra" { ((>= "1.8.0" & < "1.9.0~") | = "dev") }
2120
"coq-mathcomp-bigenough" {>= "1.0.0" & < "1.1.0~"}
22-
"coq-mathcomp-finmap" {>= "1.1.0" & < "1.2.0~"}
21+
"coq-mathcomp-finmap" {>= "1.2.0" & < "1.3.0~"}
2322
]
2423
tags: [
2524
"keyword:multinomials"
@@ -29,3 +28,4 @@ tags: [
2928
"date:2016"
3029
"logpath:SsrMultinomials"
3130
]
31+
synopsis: "A Multivariate polynomial Library for the Mathematical Components Library"

‎src/monalg.v‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -80,24 +80,24 @@ Section ClassDef.
8080
Record class_of T := Class
8181
{ base : Choice.class_of T; mixin : mixin_of T }.
8282

83-
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
83+
Structure type := Pack {sort; _ : class_of sort}.
8484

8585
Local Coercion base : class_of >-> Choice.class_of.
8686
Local Coercion sort : type >-> Sortclass.
8787

8888
Variables (T : Type) (cT : type).
8989

90-
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
91-
Definition clone c of phant_id class c := @Pack T c T.
90+
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
91+
Definition clone c of phant_id class c := @Pack T c.
9292

93-
Let xT := let: Pack T _ _ := cT in T.
93+
Let xT := let: Pack T _ := cT in T.
9494
Notation xclass := (class : class_of xT).
9595

9696
Definition pack m :=
97-
fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m) T.
97+
fun bT b & phant_id (Choice.class bT) b => Pack (@Class T b m).
9898

99-
Definition eqType := @Equality.Pack cT xclass xT.
100-
Definition choiceType := @Choice.Pack cT xclass xT.
99+
Definition eqType := @Equality.Pack cT xclass.
100+
Definition choiceType := @Choice.Pack cT xclass.
101101

102102
End ClassDef.
103103

@@ -140,26 +140,26 @@ Record class_of (M : Type) : Type := Class {
140140
mixin : commutative (MonomialDef.mul base)
141141
}.
142142

143-
Structure type := Pack {sort; _ : class_of sort; _ : Type}.
143+
Structure type := Pack {sort; _ : class_of sort}.
144144

145145
Local Coercion base : class_of >-> MonomialDef.class_of.
146146
Local Coercion sort : type >-> Sortclass.
147147

148148
Variables (T : Type) (cT : type).
149149

150-
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
151-
Definition clone c of phant_id class c := @Pack T c T.
150+
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
151+
Definition clone c of phant_id class c := @Pack T c.
152152

153-
Let xT := let: Pack T _ _ := cT in T.
153+
Let xT := let: Pack T _ := cT in T.
154154
Notation xclass := (class : class_of xT).
155155

156156
Definition pack mul0 (m0 : @commutative T T mul0) :=
157157
fun bT b & phant_id (MonomialDef.class bT) b =>
158-
fun m & phant_id m0 m => Pack (@Class T b m) T.
158+
fun m & phant_id m0 m => Pack (@Class T b m).
159159

160-
Definition eqType := @Equality.Pack cT xclass xT.
161-
Definition choiceType := @Choice.Pack cT xclass xT.
162-
Definition monomType := @MonomialDef.Pack cT xclass xT.
160+
Definition eqType := @Equality.Pack cT xclass.
161+
Definition choiceType := @Choice.Pack cT xclass.
162+
Definition monomType := @MonomialDef.Pack cT xclass.
163163

164164
End ClassDef.
165165

‎src/mpoly.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2120,7 +2120,7 @@ apply/uniq_perm_eq=> //; first rewrite map_inj_uniq //.
21202120
move=> m'; apply/idP/idP; last first.
21212121
case/mapP=> mp mp_in_p ->; rewrite mcoeff_msupp.
21222122
by rewrite mcoeffMX -mcoeff_msupp.
2123-
move/msuppM_le; rewrite msuppX /= => /allpairsP.
2123+
move/msuppM_le; rewrite msuppX => /allpairsP.
21242124
case=> [[p1 p2]] /=; rewrite mem_seq1; case=> p1_in_p.
21252125
move/eqP=> <- ->; apply/mapP; exists p1=> //.
21262126
by rewrite Monoid.mulmC.

0 commit comments

Comments
 (0)