issues
search
math-comp
/
mczify
Micromega tactics for Mathematical Components
23
stars
8
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Update CI
#57
pi8027
closed
1 day ago
0
adapt to MC#1256
#56
Tragicus
closed
4 weeks ago
1
Update CI
#55
pi8027
closed
3 months ago
0
Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01
#54
rtetley
closed
4 months ago
2
Update CI
#53
pi8027
closed
7 months ago
0
Update CI
#52
pi8027
closed
10 months ago
0
Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10
#51
MSoegtropIMC
closed
10 months ago
2
Update CI
#50
pi8027
closed
11 months ago
0
Package broken or opam bounds incorrect with mathcomp/mathcomp:1.17.0-coq-dev
#49
JasonGross
closed
1 year ago
1
Add morphism instances for N.to_nat and N.of_nat
#48
pi8027
closed
1 year ago
0
`N` forms a semiring
#47
pi8027
closed
1 year ago
2
Adapt to math-comp/math-comp#980
#46
pi8027
closed
1 year ago
0
Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03
#45
MSoegtropIMC
closed
1 year ago
1
Release compatible with Coq 8.17
#44
proux01
closed
1 year ago
3
Update CI
#43
pi8027
closed
1 year ago
0
Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09
#42
MSoegtropIMC
closed
2 years ago
1
Update CI
#41
pi8027
closed
2 years ago
0
Adapt w.r.t. coq/coq#16004.
#40
ppedrot
closed
2 years ago
1
Port to Hierarchy Builder
#39
proux01
closed
1 year ago
1
Fix dependencies
#38
pi8027
closed
2 years ago
0
Update CI
#37
pi8027
closed
2 years ago
0
Please pick the version you prefer for Coq 8.15 in Coq Platform 2022.02
#36
MSoegtropIMC
closed
2 years ago
2
Update CI
#35
pi8027
closed
2 years ago
0
Add more instances and test cases
#34
pi8027
closed
2 years ago
0
More test cases
#33
pi8027
closed
2 years ago
0
Add support for `eq_op : rel N`
#32
pi8027
closed
2 years ago
0
Update CI
#31
pi8027
closed
2 years ago
0
Update CI and dependencies
#30
pi8027
closed
2 years ago
1
Add support for NatTrec and nat <-> BinNums conversion
#29
pi8027
closed
2 years ago
0
Fix Makefile
#28
pi8027
closed
2 years ago
0
Add support for `GRing.unit`
#27
pi8027
closed
2 years ago
0
Add the `ssrZ` library
#26
pi8027
closed
2 years ago
7
`rewrite -> unfold_in in *` in `zify_pre_hook` is incomplete
#25
pi8027
closed
2 years ago
0
Add a new example: zagier.v
#24
pi8027
closed
2 years ago
0
Update CI
#23
pi8027
closed
2 years ago
0
Test suite
#22
pi8027
closed
3 years ago
0
Performence issue
#21
thery
opened
3 years ago
12
`Z` <-> `int` correspondence, structure instances for `Z`, and bridging `ssralg` to `ring`/`field` tactics
#20
pi8027
closed
2 years ago
0
Update CI
#19
pi8027
closed
3 years ago
0
Pair equality handling
#18
ecranceMERCE
opened
3 years ago
2
Split the zify instances into two parts: one for ssreflect and another for algebra
#17
pi8027
closed
3 years ago
0
Test suite
#16
pi8027
opened
3 years ago
2
Missing instances
#15
pi8027
opened
3 years ago
0
nice example
#14
thery
closed
2 years ago
2
Setup CI
#13
pi8027
closed
3 years ago
0
Inclusion of mczify into Coq platform 8.12.0
#12
MSoegtropIMC
closed
2 years ago
19
Support several versions of MathComp by splitting zify.v
#11
pi8027
closed
2 years ago
3
Adjust two proofs to mathcomp 1.11 (should also work with 1.10)
#10
MSoegtropIMC
closed
4 years ago
1
The 8.11 branch does not compile with mathcomp 1.11.0
#9
MSoegtropIMC
closed
4 years ago
6
Reimplement the pre-hook properly by relying on coq/coq#12552
#8
pi8027
closed
4 years ago
0
Next