Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / math-comp/finmap issues and pull requests

#112 - Add lemmas about imfset

Pull Request - State: open - Opened by ana-borges 4 months ago

#111 - [CI] Add Coq 8.19

Pull Request - State: closed - Opened by proux01 8 months ago - 1 comment

#110 - Update meta.yml

Pull Request - State: closed - Opened by pi8027 10 months ago

#109 - Adapt to math-comp/math-comp#1133 (replace fun_scope with function_scope)

Pull Request - State: closed - Opened by pi8027 10 months ago - 2 comments

#108 - Generic sets mathcomp2

Pull Request - State: open - Opened by affeldt-aist over 1 year ago

#107 - Experimental set

Pull Request - State: closed - Opened by affeldt-aist over 1 year ago

#106 - Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

Issue - State: closed - Opened by MSoegtropIMC over 1 year ago - 1 comment

#105 - remove old toolbox setup

Pull Request - State: closed - Opened by CohenCyril over 1 year ago

#104 - add the theorem codomf_cat

Pull Request - State: closed - Opened by thery over 1 year ago - 2 comments

#103 - Update the version constraint on Coq and CI

Pull Request - State: closed - Opened by pi8027 almost 2 years ago - 1 comment

#102 - Missing coercion from finSet to finType

Issue - State: open - Opened by rhz almost 2 years ago

#101 - two lemmas from infotheo

Pull Request - State: closed - Opened by affeldt-aist almost 2 years ago

#99 - add mathcomp 1.16 to CI

Pull Request - State: closed - Opened by affeldt-aist about 2 years ago

#98 - drop old verions

Pull Request - State: closed - Opened by affeldt-aist about 2 years ago

#97 - Adapt to math-comp/math-comp#898

Pull Request - State: closed - Opened by proux01 about 2 years ago - 1 comment

#96 - Deprecated lemmas

Pull Request - State: closed - Opened by affeldt-aist over 2 years ago

#95 - Fix the _.[_ <- _] notation priorities w.r.t Coq.Parray

Pull Request - State: closed - Opened by strub over 2 years ago

#94 - Adapt w.r.t. coq/coq#10764.

Pull Request - State: closed - Opened by ppedrot over 2 years ago - 2 comments

#92 - Allow Coq 8.15 and MathComp 1.14 in the OPAM file, add more CI tests

Pull Request - State: closed - Opened by pi8027 almost 3 years ago

#91 - update CI for mathcomp-1.13 and remove bigenough dependency

Pull Request - State: closed - Opened by chdoc almost 3 years ago

#90 - Remove dependency on bigenough

Pull Request - State: closed - Opened by eupp almost 3 years ago - 4 comments

#89 - remove bigenough dependency

Issue - State: closed - Opened by chdoc almost 3 years ago

#88 - Generalize `imfset_comp` lemma

Pull Request - State: closed - Opened by volodeyka almost 3 years ago - 3 comments

#87 - countType instances for fmap and fsfun

Pull Request - State: closed - Opened by eupp almost 3 years ago - 1 comment

#86 - Please pick the version you prefer for Coq 8.14 in Coq Platform 2021.11

Issue - State: closed - Opened by MSoegtropIMC almost 3 years ago - 1 comment

#85 - Need `Coq.Program.Tactics.`

Issue - State: open - Opened by corwin-of-amber almost 3 years ago - 3 comments

#84 - tentative port of `finmap.v` to HB

Pull Request - State: closed - Opened by affeldt-aist over 3 years ago - 1 comment

#83 - finmap is compatible with Coq 8.13

Pull Request - State: closed - Opened by pi8027 over 3 years ago

#82 - files with headers

Pull Request - State: open - Opened by CohenCyril almost 4 years ago - 1 comment

#81 - release tool (to be exported)

Pull Request - State: closed - Opened by CohenCyril almost 4 years ago

#80 - finmap for 1.12?

Issue - State: closed - Opened by thery almost 4 years ago - 2 comments

#79 - Preparing next release

Pull Request - State: closed - Opened by CohenCyril almost 4 years ago - 4 comments

#79 - Preparing next release

Pull Request - State: closed - Opened by CohenCyril almost 4 years ago - 4 comments

#78 - Update .travis.yml

Pull Request - State: closed - Opened by CohenCyril almost 4 years ago

#77 - Fix w.r.t. math-comp/math-comp#671: avoid use of join_idP(l|r)

Pull Request - State: closed - Opened by pi8027 almost 4 years ago - 3 comments

#75 - partition_disjoint_bigfcup lemma

Pull Request - State: closed - Opened by affeldt-aist almost 4 years ago - 1 comment

#74 - minor fixes

Pull Request - State: closed - Opened by affeldt-aist about 4 years ago

#73 - Notation issues for `imfset`

Issue - State: open - Opened by chdoc about 4 years ago - 2 comments

#72 - add setfs function to update an fsfun, add key setfs lemmas

Pull Request - State: closed - Opened by palmskog about 4 years ago - 6 comments

#71 - Coq 8.12 ok in opam file

Pull Request - State: closed - Opened by affeldt-aist about 4 years ago

#70 - fix-travis

Pull Request - State: closed - Opened by CohenCyril over 4 years ago

#69 - Update .travis.yml to integrate coq 8.12

Pull Request - State: closed - Opened by CohenCyril over 4 years ago

#68 - Update description

Issue - State: open - Opened by affeldt-aist over 4 years ago - 1 comment

#67 - Update w.r.t. MathComp 1.11.0+beta1

Pull Request - State: closed - Opened by affeldt-aist over 4 years ago

#66 - add docker images for mathcomp 1.11.0

Pull Request - State: closed - Opened by affeldt-aist over 4 years ago

#65 - Add finmap to Coq's CI

Issue - State: open - Opened by anton-trunov over 4 years ago

#64 - compatibility with mathcomp-dev and lost with mathcomp < 1.9.0

Pull Request - State: closed - Opened by CohenCyril over 4 years ago

#63 - Add `Reserved Notation`s in finmap.v

Pull Request - State: closed - Opened by pi8027 over 4 years ago - 1 comment

#62 - compilation error due to Notation "[ 'fset[' key ] E | x : A , y : B ]"

Issue - State: closed - Opened by erikmd over 4 years ago - 2 comments

#61 - Following the recent changes from MathComp

Pull Request - State: closed - Opened by pi8027 over 4 years ago - 7 comments

#60 - Following changes from mathcomp branch experiment/order

Pull Request - State: closed - Opened by CohenCyril almost 5 years ago

#59 - Which version works with mathcomp 1.9? and the upcoming?

Issue - State: closed - Opened by amahboubi almost 5 years ago - 1 comment

#58 - Anticipating support for sign tables in analysis and realclosed

Pull Request - State: closed - Opened by CohenCyril almost 5 years ago - 1 comment

#57 - removed useless premises in finSet_rect

Pull Request - State: closed - Opened by strub almost 5 years ago

#56 - Fset of a fintype is now a fintype : fixes issue #55.

Pull Request - State: closed - Opened by Nemeras about 5 years ago - 1 comment

#55 - Fset of a fintype

Issue - State: open - Opened by Nemeras about 5 years ago - 3 comments

#54 - keeping ^l for (min|max)lexi

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#53 - fixing min and max

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#52 - fixup

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#51 - bugfixes + tuple

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#50 - bugfixes

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#49 - reshufflings and renamings

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#48 - Fix CI

Pull Request - State: closed - Opened by CohenCyril over 5 years ago - 1 comment

#47 - fix order

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#46 - totalType in ProdLexOrder and SeqProdOrder

Issue - State: closed - Opened by mituharu over 5 years ago - 1 comment

#45 - New order

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#44 - update opam and travis

Pull Request - State: closed - Opened by CohenCyril over 5 years ago - 1 comment

#43 - fix for mathcomp master

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#42 - nix shell

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#41 - nix shell

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#40 - fix compatibility with `seq` renaming

Pull Request - State: closed - Opened by ggonthier over 5 years ago - 3 comments

#39 - anticipate `seq` lemma renamings

Pull Request - State: closed - Opened by ggonthier over 5 years ago

#38 - replace `mkPredType` with `PredType`

Pull Request - State: closed - Opened by ggonthier over 5 years ago
Labels: bug

#37 - Update .travis.yml to remove mathcomp-1.8.0-coq-dev test

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#36 - Compatibility with ssrbool update coq/coq#9995

Pull Request - State: closed - Opened by ggonthier over 5 years ago - 1 comment

#35 - better opam

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#34 - Compatible with mathcomp 1.8.0

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#33 - allow mathcomp dev in finmap

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#32 - Compatibility with math-comp master

Pull Request - State: closed - Opened by proux01 over 5 years ago - 6 comments

#31 - fix Makefile.common

Pull Request - State: closed - Opened by CohenCyril over 5 years ago

#30 - compilation with mathcomp (Mon Jan 28 commit) and coq 8.9

Pull Request - State: closed - Opened by affeldt-aist over 5 years ago - 1 comment

#29 - [opam]: add dev-repo

Pull Request - State: closed - Opened by anton-trunov almost 6 years ago - 3 comments

#28 - Should "unit_irrelevance" fact be moved elsewhere?

Issue - State: open - Opened by anton-trunov about 6 years ago - 9 comments

#27 - bind finmap to the bigenough machinery

Pull Request - State: closed - Opened by strub about 6 years ago

#26 - Simplification in imset2 should be locked

Issue - State: open - Opened by hivert about 6 years ago - 1 comment

#25 - Plain not distributive lattices

Issue - State: open - Opened by hivert about 6 years ago - 11 comments

#24 - subtype in order/lattices

Issue - State: open - Opened by hivert about 6 years ago

#23 - Reverse/Dual/Opposite of an order

Issue - State: open - Opened by hivert about 6 years ago

#22 - V1.1

Pull Request - State: closed - Opened by CohenCyril about 6 years ago

#21 - finmap should compile even with mathcomp1.6

Pull Request - State: closed - Opened by CohenCyril about 6 years ago

#20 - Towards v1.1.0, strictly better, not completely backward compatible

Pull Request - State: closed - Opened by CohenCyril about 6 years ago

#19 - Towards version 1.0.0 (compatible with dev up to now)

Pull Request - State: closed - Opened by CohenCyril about 6 years ago

#18 - better doc

Pull Request - State: closed - Opened by CohenCyril about 6 years ago

#17 - Cleaning some whitespaces

Pull Request - State: closed - Opened by CohenCyril about 6 years ago

#16 - Order-preserving morphisms

Issue - State: open - Opened by ejgallego almost 7 years ago - 4 comments

#15 - Not compatible with Coq.8.7

Issue - State: closed - Opened by ildyria almost 7 years ago - 10 comments

#14 - proof of fset2P should not rely on intuition

Pull Request - State: closed - Opened by ybertot about 7 years ago - 1 comment