coq-community/corn issues and pull requests

#95 - Split min, max and powers

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

#94 - Overlay for PR 12287

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

#93 - overlay for coq/coq#12162 after merge of coq/coq#12008

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

#92 - overlay for coq/coq#12162

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

#91 - overlay for coq/coq#12190

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

#90 - Dominated convergence theorem

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

#89 - Skip Opaque_algebra.v in the build

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

#88 - Constructive measure theory

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

#87 - Remove or replace leftover SearchAbout.

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

#86 - Some cleaning

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

#85 - Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)

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

#84 - fix typo in CSetoids.tex

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

#83 - Do not use “try auto with *”.

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

#82 - Be careful with automated proof search that is expected to fail

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

#81 - Explain how to build Corn and its dependencies from the sources

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

#80 - Application for maintainer position

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

#79 - Avoid relying on `Export` bugs (again)

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

#78 - Integration of corn real numbers into Coq's standard library

Issue - State: closed - Opened by VincentSe about 5 years ago - 10 comments

#77 - typo. it's github.com not github/com.

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

#76 - Add 8.10 support / testing.

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

#75 - Avoid relying on `Export` bugs

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

#74 - Fundamental theorem of algebra :: location?

Issue - State: open - Opened by OrenGitHub over 5 years ago - 2 comments

#73 - Adapt to Coq's PR #9854

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

#72 - [coq] Adapt to coq/coq#8764

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

#71 - Make explicit some uses of Zpos

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

#70 - Use Z.log2 instead of the deprecated Zlogarithm

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

#69 - Make coercions explicit

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

#68 - many Admitted instances

Issue - State: closed - Opened by gares over 5 years ago - 1 comment
Labels: help wanted

#67 - Add explicit {struct} annotation to avoid Coq expensive guessing

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

#66 - Introduce meta.yml file, in place of description file.

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

#65 - Make trivial instances explicit

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

#64 - Name premises to avoid collision

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

#63 - Remove deprecated arithmetic notations

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

#62 - Remove all or most compatibility-notation warnings.

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

#61 - updating version number

Pull Request - State: closed - Opened by spitters about 6 years ago - 10 comments

#60 - Fix Corn build failure following math-classes update.

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

#59 - Corn is broken following recent changes in math-classes

Issue - State: closed - Opened by Zimmi48 over 6 years ago

#58 - Std lib ommisions

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

#57 - Syntax error when installing with opam

Issue - State: closed - Opened by nathan-koskas over 6 years ago - 16 comments

#56 - Make Travis pick up math-classes master

Pull Request - State: closed - Opened by maximedenes over 6 years ago - 3 comments

#55 - Replace Fourier with Lra.

Pull Request - State: closed - Opened by maximedenes over 6 years ago - 20 comments

#54 - Fix #52: `cofix` tactic without a name is deprecated.

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

#53 - Adapt to the deprecation of positive coinductive types.

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

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

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

#51 - Backward compatible fix for coq/coq#7451.

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

#50 - Get rid of `'` notation

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

#49 - Change Implicit Arguments to Arguments

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

#48 - Removed the ssreflect dependency and fixed some "Admitted"

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

#47 - updated SConstruct for the new version of Liouville

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

#46 - Updated proof of Liouville's theorem

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

#45 - Fix obsolete vernacular syntax for locality.

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

#44 - Travis

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

#43 - V8.6

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

#42 - corn : switch to the external Bignums library

Pull Request - State: closed - Opened by letouzey over 7 years ago - 1 comment

#41 - fix unused variable name warnings

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

#40 - Make proofs oblivious to the changes in the definition of IZR.

Pull Request - State: closed - Opened by silene over 7 years ago - 1 comment

#39 - Notation Clash

Issue - State: closed - Opened by rnrand almost 8 years ago - 5 comments

#38 - [math-classes] Non-commutative (semi)rings

Issue - State: open - Opened by urkud almost 8 years ago - 2 comments

#37 - [math-classes] Additional axiom on inner product spaces: 0 = ⟨v,v⟩ iff v = mon_unit

Issue - State: closed - Opened by langston-barrett almost 8 years ago - 2 comments

#36 - [math-classes] Should the inner product be proper with respect to equivalence?

Issue - State: closed - Opened by langston-barrett almost 8 years ago - 2 comments

#35 - [math-classes] Some proofs are notation-dependent

Issue - State: closed - Opened by langston-barrett almost 8 years ago - 2 comments

#34 - travis: fix cached builds

Pull Request - State: closed - Opened by langston-barrett almost 8 years ago - 2 comments

#33 - Remove "Git checkout and submodules" from README, and OPAM info

Issue - State: closed - Opened by langston-barrett almost 8 years ago - 1 comment

#32 - Travis CI

Pull Request - State: closed - Opened by langston-barrett almost 8 years ago

#31 - Travis CI

Issue - State: closed - Opened by langston-barrett almost 8 years ago - 3 comments

#30 - Getting started with math-classes

Issue - State: closed - Opened by langston-barrett about 8 years ago - 8 comments

#29 - adding "Make" and "Makefile"

Pull Request - State: closed - Opened by ghost over 8 years ago

#28 - adding "Make" and "Makefile"

Pull Request - State: closed - Opened by ghost over 8 years ago

#27 - Fixing compilaton wrt. Coq trunk (244d7a9)

Pull Request - State: closed - Opened by ghost over 8 years ago

#26 - Fixing compilaton wrt. Coq 8.5 (d2f9a45)

Pull Request - State: closed - Opened by ghost over 8 years ago

#25 - fixing compilation (wrt. Coq trunk)

Pull Request - State: closed - Opened by ghost over 8 years ago - 3 comments

#24 - Make import statements absolute and other small changes

Pull Request - State: closed - Opened by bmsherman over 8 years ago - 1 comment

#23 - typeclass resolution confusing addition and multiplication

Issue - State: closed - Opened by aa755 almost 9 years ago - 7 comments

#22 - README in MarkDown with OPAM instructions

Pull Request - State: closed - Opened by clarus almost 9 years ago - 1 comment

#21 - minimal patch to compile CoRN on Mac and Win following recent MathClasses patch

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

#20 - Updating README, resolving #19

Pull Request - State: closed - Opened by spitters over 9 years ago

#19 - README out of date

Issue - State: closed - Opened by jldodds over 9 years ago - 1 comment

#18 - DistanceMetricSpace never used

Issue - State: closed - Opened by aa755 almost 10 years ago

#17 - many lemmas about sin, cos, arctan.

Pull Request - State: closed - Opened by aa755 almost 10 years ago - 1 comment

#16 - universe inconsistency

Issue - State: closed - Opened by aa755 almost 10 years ago - 1 comment

#15 - Pointwise and SubCRing constructors

Pull Request - State: closed - Opened by aa755 almost 10 years ago - 1 comment

#14 - 3 lemmas. 1) intervals are convex 2) Min is contained in any interval containing the 2 args 3) same for max

Pull Request - State: closed - Opened by aa755 almost 10 years ago

#13 - added the Weak_IVTQ lemma which is a stronger variant of CoRN.ftc.Stron...

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

#12 - Compilation problem with Coq 8.4pl5

Issue - State: closed - Opened by vzaliva almost 10 years ago

#11 - syntax error when compiling on Ubuntu

Issue - State: closed - Opened by wolvre almost 10 years ago - 1 comment

#10 - Missing reference 'ifb' under Coq 8.4pl5

Issue - State: closed - Opened by jwiegley about 10 years ago - 1 comment

#9 - Building on OS X

Issue - State: closed - Opened by jwiegley about 10 years ago - 3 comments

#8 - reading order

Issue - State: open - Opened by aa755 about 10 years ago

#7 - fixed some windows case insensitivity issues

Pull Request - State: closed - Opened by aa755 about 10 years ago

#6 - Building on Windows

Issue - State: closed - Opened by aa755 about 10 years ago - 3 comments

#5 - Preparation for Opam

Pull Request - State: closed - Opened by clarus about 10 years ago

#4 - Trunk

Pull Request - State: closed - Opened by spitters about 10 years ago

#3 - Trunk

Pull Request - State: closed - Opened by spitters about 10 years ago

#2 - Trunk

Pull Request - State: closed - Opened by spitters about 10 years ago

#1 - Update to 8.4 beta

Pull Request - State: closed - Opened by wires almost 13 years ago

GitHub / coq-community/corn issues and pull requests