Ecosyste.ms: Issues

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

GitHub / coq-community/corn issues and pull requests

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

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

#207 - Update maintainer list in README.

Pull Request - State: closed - Opened by Zimmi48 3 months ago

#206 - remove unneeded Ndigits dependency (adapt to coq/coq#18936)

Pull Request - State: closed - Opened by andres-erbsen 7 months ago

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

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

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

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

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

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

#202 - Adapt to Coq/Coq#18164

Pull Request - State: closed - Opened by Villetaneuse about 1 year ago - 4 comments

#201 - Update testing to Coq 8.18.

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

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

Issue - State: closed - Opened by rtetley about 1 year ago - 3 comments

#199 - Adapting to interpretation of (x:T) now activating scope for T if any.

Pull Request - State: closed - Opened by proux01 about 1 year ago

#198 - Remove deprecated options/flags

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

#197 - Remove conditional from configure.sh

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

#196 - No need to check COQ version in configure.sh

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

#195 - Deprecating notation

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

#194 - Deprecated notations

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

#193 - More notation deprecations

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

#192 - More notation deprecations

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

#191 - More deprecations of notation

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

#190 - Deprecate le_not_lt for Nat.le_ngt

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

#189 - More notation deprecations.

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

#188 - More fixes for deprecated notation warnings

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

#187 - Remove more deprecated notations

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

#186 - Remove more deprecated notations.

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

#185 - Replace deprecated proof components

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

#184 - Replace max with Nat.max throughout.

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

#183 - Source lt/le/lt_le/le_lt_trans from library.

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

#182 - Use `bc` for version comparison in configure.sh

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

#181 - Comments and bullets in compact_is_totally_bounded.

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

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

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

#179 - Remove support for untested versions of Coq.

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

#178 - Update Picard.v

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

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

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

#176 - Adapt to coq/coq#16920

Pull Request - State: closed - Opened by olaure01 almost 2 years ago - 2 comments

#175 - Adapt w.r.t. coq/coq#16904.

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

#173 - Please create a tag for Coq 8.16 in Coq Platform 2022.09

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

#172 - Unclear licensing

Issue - State: open - Opened by SnarkBoojum over 2 years ago - 1 comment

#171 - improved auto goal selection

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

#170 - Remove compatibility with Coq < 8.11 and add testing for recent versions.

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

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

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

#168 - Avoid relying on Coq bug #3556

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

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

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

#166 - Adapt w.r.t. coq/coq#15442.

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

#165 - added more IR_***_as_R lemmas

Pull Request - State: closed - Opened by jakezweifler about 3 years ago - 1 comment

#164 - Missing translations from IR to R

Issue - State: open - Opened by jakezweifler about 3 years ago - 1 comment

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

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

#162 - Please use qualified paths in the example files

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

#161 - Update meta.yml and CI to test Coq 8.13.

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

#160 - New release?

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

#159 - Future proof Zlcm.v and ZMod.v for

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

#158 - Adapt to coq/coq#14041

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

#157 - Compute arctan with inductive streams

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

#156 - Stop requiring the Omega module.

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

#155 - Remove last calls to omega.

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

#154 - Remove many calls to omega.

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

#152 - Compute sine with inductive streams

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

#151 - Simplify two proofs and stop using double induction.

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

#150 - Fix examples

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

#149 - Improve fuel of exponential

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

#148 - Switch from Travis CI to GitHub Actions.

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

#147 - Stop using deprecated firstorder using syntax.

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

#146 - Remove coinductive streams in exponential

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

#145 - Replace coinductive streams by inductive streams

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

#143 - Sparse rasters

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

#142 - Replace Vector by list in rasters

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

#141 - Replace nat by positive in rasters

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

#140 - Fix extraction of sine and cosine

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

#139 - Replace CoFixpoint by Fixpoint in compacts

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

#138 - Prove that compact approximations are correct

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

#137 - Remove RSetoid from metric spaces

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

#136 - Simplify almostIn

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

#135 - Simplify InFinEnumC

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

#134 - Faster plot of circle

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

#133 - Faster complex numbers

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

#132 - Fix plot of circle

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

#131 - Fix admitted lemmas in faster reals

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

#130 - Fix some admitted lemmas

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

#129 - Fix dump, a plugin that plots subsets of the plane

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

#128 - Proof that plots of located subsets cover the subsets

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

#127 - Plot located subsets of the plane

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

#126 - Consequences of Markov's principle on constructive reals

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

#125 - Located subsets of metric spaces

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

#124 - Move stability into the definition of metric spaces

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

#123 - dump.ml does not compile anymore

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

#122 - Cut algebraic hierarchy from FinEnum

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

#121 - Faster implementation of inject_Q_AR

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

#120 - Faster implementation of ARabs

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

#119 - Listing and preserving Corn-related publications

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

#118 - Put typeclass context in a section for ConstructiveFasterReals

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

#117 - Prove that faster reals implement stdlib constructive reals

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

#116 - Cut algebraic hierarchy from ARArith

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

#115 - Prove that fast reals are Cauchy complete

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

#114 - Put fast reals in sort Set instead of Type

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

#113 - Relicense constructive measure theory

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

#100 - Remove algebraic hierarchy from Qmetric

Pull Request - State: closed - Opened by VincentSe over 4 years ago - 12 comments

#99 - Replace CoRN's license by Coq's license

Pull Request - State: open - Opened by VincentSe over 4 years ago - 38 comments

#98 - Create README.md

Pull Request - State: closed - Opened by spitters over 4 years ago - 15 comments

#97 - Regenerate files from latest templates.

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

#96 - Avoid ring collision on Z

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