coq-community/math-classes issues and pull requests

#131 - Adapt to https://github.com/coq/coq/pull/19530

Pull Request - State: closed - Opened by proux01 6 days ago - 1 comment

#130 - Update maintainer list in README.

Pull Request - State: closed - Opened by Zimmi48 about 1 month ago

#129 - Port Coq code to use 'done' tactic instead of 'easy' and benchmark

Pull Request - State: open - Opened by ndcroos about 2 months ago - 6 comments

#128 - Port Coq code to use done tactic instead of easy and benchmark

Issue - State: open - Opened by palmskog 3 months ago - 4 comments
Labels: help wanted

#127 - Adapt to https://github.com/coq/coq/pull/18880

Pull Request - State: closed - Opened by proux01 5 months ago

#126 - Remove the few instances of non-global hint declarations.

Pull Request - State: closed - Opened by ppedrot 6 months ago

#125 - Please create a tag for Coq 8.19 in Coq Platform 2024.01

Issue - State: closed - Opened by rtetley 6 months ago - 4 comments

#124 - Support Coq 8.19

Issue - State: closed - Opened by SnarkBoojum 7 months ago - 4 comments

#123 - Adapt to https://github.com/coq/coq/pull/18590

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

#122 - Adapt to Coq PR #17832: syntax of choice in rewstrategy expects arguments at atomic level

Pull Request - State: closed - Opened by herbelin 11 months ago - 1 comment

#121 - Remove deprecated files in Coq.Arith

Pull Request - State: closed - Opened by Villetaneuse 11 months ago - 2 comments

#120 - Please create a tag for Coq 8.18 in Coq Platform 2023.10

Issue - State: closed - Opened by rtetley 12 months ago - 4 comments

#119 - Introducing CI for Coq 8.18.

Pull Request - State: closed - Opened by Zimmi48 12 months ago - 2 comments

#118 - Adapt to https://github.com/coq/coq/pull/6134

Pull Request - State: closed - Opened by proux01 12 months ago

#117 - Adapt w.r.t. coq/coq#17564.

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

#116 - Test Coq 8.17, clean up stale files.

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

#115 - Please create a tag for Coq 8.17 in Coq Platform 2023.03

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

#114 - adapt to coq/coq#17133

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

#113 - Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09

Issue - State: closed - Opened by MSoegtropIMC about 2 years ago - 7 comments

#112 - Drop compatibility testing with 8.6-8.10, test 8.16.

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

#111 - Adapt w.r.t. coq/coq#16004.

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

#110 - Test compatibility with Coq versions up to 8.15.

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

#109 - Please create a tag for Coq 8.15 in Coq Platform 2022.02

Issue - State: closed - Opened by MSoegtropIMC over 2 years ago - 5 comments

#108 - 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 - 2 comments

#107 - Inclusion in the Coq Platform

Issue - State: closed - Opened by MSoegtropIMC almost 3 years ago - 2 comments

#106 - Please suggest example file for Coq Platform "smoke test kit"

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

#105 - Fix w.r.t. coq/coq#14679.

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

#104 - Fix w.r.t. coq/coq#14876.

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

#103 - Start testing again from Coq 8.6.

Pull Request - State: closed - Opened by Zimmi48 about 3 years ago

#102 - make compilation work for coq <= 8.10

Pull Request - State: closed - Opened by larsr about 3 years ago - 3 comments

#101 - Generating automation by reflection from universal algebra?

Issue - State: closed - Opened by mdgeorge4153 over 3 years ago - 1 comment

#100 - added group tactic and automated some proofs in groups.v

Pull Request - State: closed - Opened by mdgeorge4153 over 3 years ago - 4 comments

#99 - RingOrder for types with decidable equality

Issue - State: open - Opened by mdgeorge4153 over 3 years ago - 2 comments

#98 - compatibility with PR #14037

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

#97 - coq 8.13 support

Issue - State: closed - Opened by vzaliva over 3 years ago - 9 comments

#96 - Fix performance bug

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

#95 - Future proof EuclidSpec

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

#94 - Remove last use of omega.

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

#93 - Switch from Travis CI to GitHub Actions.

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

#92 - Adapt to coq/coq#13188 (Default disable automatic generalization of Instance type)

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

#91 - Remove the reliance on forward class hints

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

#90 - update metadata and templates for 8.12 support

Pull Request - State: closed - Opened by palmskog about 4 years ago - 1 comment

#89 - Release for Coq 8.12

Issue - State: closed - Opened by palmskog about 4 years ago - 3 comments

#88 - switch to MIT license

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

#87 - Changing to an SPDX-identifiable license

Issue - State: closed - Opened by palmskog about 4 years ago - 4 comments

#86 - Regenerate files from latest templates.

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

#85 - [coq] use ListNotations explicitly

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

#84 - Update meta.yml to test Coq 8.11 (and wrt latest templates).

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

#83 - Coq-8.11 support

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

#82 - Do not expect “firstorder” to solve boolean goals

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

#81 - Avoid relying on `Add Field` calling `Add Ring`.

Pull Request - State: open - Opened by maximedenes over 4 years ago - 5 comments

#80 - stdlib_rationals: explicitly require and import ZArith

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

#79 - PR coq/coq#10762 overlay

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

#78 - Fix for a new rapply tactic

Pull Request - State: closed - Opened by JasonGross about 5 years ago - 2 comments

#77 - Fix w.r.t. coq/coq#10764.

Pull Request - State: closed - Opened by ppedrot about 5 years ago

#76 - Fix name of opam file to correspond to name in opam archive.

Pull Request - State: closed - Opened by Zimmi48 about 5 years ago

#75 - Add one line synopsis and several lines description.

Pull Request - State: closed - Opened by Zimmi48 about 5 years ago

#74 - Release a version compatible with Coq 8.10.

Issue - State: closed - Opened by Zimmi48 about 5 years ago - 3 comments

#73 - Update with latest version of templates.

Pull Request - State: closed - Opened by Zimmi48 about 5 years ago

#72 - ne_list: move the coercion into a dedicated module

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

#71 - Use coq-on-cachix repo to never rebuild the Coq package.

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

#70 - Adapt to https://github.com/coq/coq/pull/9410

Pull Request - State: closed - Opened by maximedenes over 5 years ago - 9 comments

#69 - Meta file, CI, etc.

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

#68 - Make trivial instances explicit

Pull Request - State: closed - Opened by maximedenes over 5 years ago - 13 comments

#67 - Do not rely on `Refine Instance Mode`

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

#66 - Use universe polymorphism to eliminate ua_subalgebraT.v

Issue - State: open - Opened by spitters almost 6 years ago
Labels: help wanted

#65 - Make math-classes compile without any deprecated notation warning.

Pull Request - State: closed - Opened by Zimmi48 about 6 years ago - 1 comment

#64 - updating readme

Pull Request - State: closed - Opened by spitters about 6 years ago - 1 comment

#63 - Compile with `-w "+compatibility-notation"

Issue - State: closed - Opened by Zimmi48 about 6 years ago - 2 comments

#62 - Autogenerate dependency graphs, documentation with travis

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

#61 - Rename Make into _CoqProject because of better IDE support.

Pull Request - State: closed - Opened by Zimmi48 about 6 years ago - 1 comment

#60 - Extend .gitignore.

Pull Request - State: closed - Opened by Zimmi48 about 6 years ago - 5 comments

#59 - Fix Travis (coq-released is already a remote repository).

Pull Request - State: closed - Opened by Zimmi48 about 6 years ago - 2 comments

#58 - Remove deprecated option `Set Automatic Coercions Import`.

Pull Request - State: closed - Opened by maximedenes about 6 years ago - 2 comments

#57 - master branch undocumented dependency on BigNums

Issue - State: closed - Opened by Zdancewic about 6 years ago - 2 comments

#56 - master branch does not build cleanly (Streams)

Issue - State: closed - Opened by Zdancewic about 6 years ago - 7 comments

#55 - math-classes relies on deprecated `Set Automatic Coercions Import`

Issue - State: closed - Opened by maximedenes about 6 years ago - 5 comments
Labels: help wanted

#54 - Add OPAM file

Pull Request - State: closed - Opened by maximedenes about 6 years ago - 7 comments

#53 - Fix #51: `cofix` tactic without a name is deprecated.

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

#52 - Backporting the legacy stream theory from Coq.

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

#51 - `cofix` tactic without a name is deprecated.

Issue - State: closed - Opened by ejgallego over 6 years ago - 1 comment

#50 - Add Module instance for polynomials

Pull Request - State: closed - Opened by tymmym over 6 years ago

#49 - Fix inner product space laws

Issue - State: open - Opened by langston-barrett over 6 years ago

#48 - Change Implicit Arguments to Arguments

Pull Request - State: closed - Opened by jashug over 6 years ago - 1 comment

#47 - notation overwrite warnings

Issue - State: open - Opened by vzaliva almost 7 years ago

#46 - V8.6

Pull Request - State: closed - Opened by Zimmi48 almost 7 years ago - 5 comments

#45 - V8.6

Pull Request - State: closed - Opened by spitters almost 7 years ago

#44 - Revert "Master"

Pull Request - State: closed - Opened by spitters almost 7 years ago

#43 - Master

Pull Request - State: closed - Opened by spitters almost 7 years ago

#42 - Prove that polynomials form a ring

Pull Request - State: closed - Opened by johanneskloos almost 7 years ago - 1 comment

#42 - Prove that polynomials form a ring

Pull Request - State: closed - Opened by johanneskloos almost 7 years ago - 1 comment

#41 - math-classes : switch to the external Bignums library

Pull Request - State: closed - Opened by letouzey over 7 years ago - 13 comments

#40 - fix triangle inequality for seminormed spaces

Pull Request - State: closed - Opened by langston-barrett over 7 years ago

#39 - every decfield is a vectorspace over itself

Pull Request - State: closed - Opened by langston-barrett over 7 years ago

#38 - add nonnegativity to seminorm properties

Pull Request - State: closed - Opened by langston-barrett over 7 years ago - 2 comments

GitHub / coq-community/math-classes issues and pull requests