coq-community/corn

Issues

• Please pick the version you prefer for Coq 8.20 in Coq Platform 2025.01

  #213 opened a month ago by MSoegtropIMC
  2

• Please create a tag for Coq 8.19 in Coq Platform 2024.01

  #204 opened 8 months ago by rtetley
  4

• Please create a tag for Coq 8.18 in Coq Platform 2023.10

  #200 opened a year ago by rtetley
  3

• Please create a tag for Coq 8.17 in Coq Platform 2023.03

  #177 opened 2 years ago by MSoegtropIMC
  4

• Please create a tag for Coq 8.16 in Coq Platform 2022.09

  #173 opened 2 years ago by MSoegtropIMC
  5

• Unclear licensing

  #172 opened 2 years ago by SnarkBoojum
  1

• Please use qualified paths in the example files

  #162 opened 3 years ago by MSoegtropIMC
  5

• Please create a tag for Coq 8.15 in Coq Platform 2022.02

  #167 opened 3 years ago by MSoegtropIMC
  1

• Missing translations from IR to R

  #164 opened 3 years ago by jakezweifler
  1

• Please pick the version you prefer for Coq 8.14 in Coq Platform 2021.11

  #163 opened 3 years ago by MSoegtropIMC
  5

• New release?

  #160 opened 3 years ago by larsr
  1

• Integration of corn real numbers into Coq's standard library

  #78 opened 4 years ago by VincentSe
  10

• many Admitted instances

  #68 opened 4 years ago by gares
  1

• dump.ml does not compile anymore

  #123 opened 4 years ago by gares
  9

• Listing and preserving Corn-related publications

  #119 opened 4 years ago by palmskog
  4

• Fundamental theorem of algebra :: location?

  #74 opened 6 years ago by OrenGitHub
  2

• Remove all or most compatibility-notation warnings.

  #62 opened 6 years ago by Zimmi48
  5

• Syntax error when installing with opam

  #57 opened 6 years ago by nathan-koskas
  16

• Corn is broken following recent changes in math-classes

  #59 opened 6 years ago by Zimmi48
  0

• Std lib ommisions

  #58 opened 6 years ago by spitters
  0

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

  #36 opened 8 years ago by langston-barrett
  2

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

  #37 opened 8 years ago by langston-barrett
  2

• [math-classes] Some proofs are notation-dependent

  #35 opened 8 years ago by langston-barrett
  2

• [math-classes] Non-commutative (semi)rings

  #38 opened 8 years ago by urkud
  2

• Notation Clash

  #39 opened 7 years ago by rnrand
  5

• `cofix` tactic without a name is deprecated.

  #52 opened 7 years ago by ejgallego
  0

• syntax error when compiling on Ubuntu

  #11 opened 7 years ago by wolvre
  1

• Compilation problem with Coq 8.4pl5

  #12 opened 7 years ago by vzaliva
  0

• universe inconsistency

  #16 opened 7 years ago by aa755
  1

• DistanceMetricSpace never used

  #18 opened 10 years ago by aa755
  0

• README out of date

  #19 opened 10 years ago by jldodds
  1

• typeclass resolution confusing addition and multiplication

  #23 opened 7 years ago by aa755
  7

• Getting started with math-classes

  #30 opened 8 years ago by langston-barrett
  8

• Remove "Git checkout and submodules" from README, and OPAM info

  #33 opened 8 years ago by langston-barrett
  1

• Travis CI

  #31 opened 8 years ago by langston-barrett
  3

• Building on Windows

  #6 opened 7 years ago by aa755
  3

• reading order

  #8 opened 10 years ago by aa755
  0

• Building on OS X

  #9 opened 9 years ago by jwiegley
  3

• Missing reference 'ifb' under Coq 8.4pl5

  #10 opened 10 years ago by jwiegley
  1