math-comp finmap issues

math-comp / finmap

Finite sets, finite maps, multisets and generic sets

46 stars 28 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Add lemmas about imfset

#112 ana-borges opened 5 months ago
0
[CI] Add Coq 8.19

#111 proux01 closed 9 months ago
1
Update meta.yml

#110 pi8027 closed 10 months ago
0
Adapt to math-comp/math-comp#1133 (replace fun_scope with function_scope)

#109 pi8027 closed 10 months ago
2
Generic sets mathcomp2

#108 affeldt-aist opened 1 year ago
0
Experimental set

#107 affeldt-aist closed 1 year ago
0
Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

#106 MSoegtropIMC closed 1 year ago
1
remove old toolbox setup

#105 CohenCyril closed 1 year ago
0
add the theorem codomf_cat

#104 thery closed 1 year ago
2
Update the version constraint on Coq and CI

#103 pi8027 closed 1 year ago
1
Missing coercion from finSet to finType

#102 rhz opened 1 year ago
0
two lemmas from infotheo

#101 affeldt-aist closed 1 year ago
0
Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09

#100 MSoegtropIMC closed 2 years ago
0
add mathcomp 1.16 to CI

#99 affeldt-aist closed 2 years ago
0
drop old verions

#98 affeldt-aist closed 2 years ago
0
Adapt to math-comp/math-comp#898

#97 proux01 closed 2 years ago
1
Deprecated lemmas

#96 affeldt-aist closed 2 years ago
0
Fix the _.[_ <- _] notation priorities w.r.t Coq.Parray

#95 strub closed 2 years ago
0
Adapt w.r.t. coq/coq#10764.

#94 ppedrot closed 2 years ago
2
Please pick the version you prefer for Coq 8.15 in Coq Platform 2022.02

#93 MSoegtropIMC closed 2 years ago
0
Allow Coq 8.15 and MathComp 1.14 in the OPAM file, add more CI tests

#92 pi8027 closed 2 years ago
0
update CI for mathcomp-1.13 and remove bigenough dependency

#91 chdoc closed 2 years ago
0
Remove dependency on bigenough

#90 eupp closed 2 years ago
4
remove bigenough dependency

#89 chdoc closed 2 years ago
0
Generalize `imfset_comp` lemma

#88 volodeyka closed 2 years ago
3
countType instances for fmap and fsfun

#87 eupp closed 2 years ago
1
Please pick the version you prefer for Coq 8.14 in Coq Platform 2021.11

#86 MSoegtropIMC closed 2 years ago
1
Need `Coq.Program.Tactics.`

#85 corwin-of-amber opened 3 years ago
3
tentative port of `finmap.v` to HB

#84 affeldt-aist closed 1 year ago
1
finmap is compatible with Coq 8.13

#83 pi8027 closed 3 years ago
0
files with headers

#82 CohenCyril opened 3 years ago
1
release tool (to be exported)

#81 CohenCyril closed 3 years ago
0
finmap for 1.12?

#80 thery closed 3 years ago
2
Preparing next release

#79 CohenCyril closed 3 years ago
4
Update .travis.yml

#78 CohenCyril closed 3 years ago
0
Fix w.r.t. math-comp/math-comp#671: avoid use of join_idP(l|r)

#77 pi8027 closed 3 years ago
3
Fix w.r.t. math-comp/math-comp#464 (new order structures and definitionally involutive duals)

#76 pi8027 closed 7 months ago
0
partition_disjoint_bigfcup lemma

#75 affeldt-aist closed 3 years ago
1
minor fixes

#74 affeldt-aist closed 4 years ago
0
Notation issues for `imfset`

#73 chdoc opened 4 years ago
2
add setfs function to update an fsfun, add key setfs lemmas

#72 palmskog closed 4 years ago
6
Coq 8.12 ok in opam file

#71 affeldt-aist closed 4 years ago
0
fix-travis

#70 CohenCyril closed 4 years ago
0
Update .travis.yml to integrate coq 8.12

#69 CohenCyril closed 3 years ago
0
Update description

#68 affeldt-aist opened 4 years ago
1
Update w.r.t. MathComp 1.11.0+beta1

#67 affeldt-aist closed 4 years ago
0
add docker images for mathcomp 1.11.0

#66 affeldt-aist closed 4 years ago
0
Add finmap to Coq's CI

#65 anton-trunov opened 4 years ago
0
compatibility with mathcomp-dev and lost with mathcomp < 1.9.0

#64 CohenCyril closed 4 years ago
0
Add `Reserved Notation`s in finmap.v

#63 pi8027 closed 4 years ago
1