math-comp/algebra-tactics

Issues

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

  #103 opened 3 months ago by MSoegtropIMC
  1

• ring mysteriously fails or succeeds on convertible goals

  #101 opened 7 months ago by andrew-appel
  3

• Compare variables by conversion or keyed matching

  #18 opened 3 years ago by pi8027
  6

• Revert #90

  #92 opened 7 months ago by pi8027
  2

• Please pick the version you prefer for Coq 8.19 in Coq Platform 2024.01

  #97 opened a year ago by rtetley
  2

• Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10

  #88 opened a year ago by rtetley
  5

• Add tests for reverse dependencies to CI

  #62 opened 3 years ago by pi8027
  1

• Reorganize the test-suite and examples

  #91 opened a year ago by pi8027
  0

• mathcomp2 and Sub deprecated

  #87 opened a year ago by thery
  2

• Polynomial coefficients with *: don't get recognized automatically -- one has to call -!mul_polyC by hand

  #64 opened a year ago by SnarkBoojum
  4

• Add documentation

  #61 opened a year ago by pi8027
  2

• Support for `nat` ?

  #40 opened 2 years ago by amahboubi
  3

• TODOs in `lra`

  #73 opened 2 years ago by pi8027
  1

• Commutative and non-commutative algebras

  #79 opened 2 years ago by pi8027
  1

• Please pick the version you prefer for Coq 8.17 in Coq Platform 2023.03

  #80 opened 2 years ago by MSoegtropIMC
  8

• new release/update for mathcomp 1.16

  #78 opened 2 years ago by clayrat
  2

• Abstract natural integer powers can be a problem

  #69 opened 2 years ago by SnarkBoojum
  2

• Coq's ring tactic works with semi-ring where mc.a-t doesn't

  #68 opened 2 years ago by SnarkBoojum
  2

• Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09

  #67 opened 3 years ago by MSoegtropIMC
  2

• Since there is a version 1.0.0 - should it move in Coq Platform from "extened" to "full"?

  #66 opened 3 years ago by MSoegtropIMC
  2

• Credits

  #34 opened 3 years ago by pi8027
  13

• Reflexive zify

  #63 opened 3 years ago by pi8027
  4

• Release 1.0

  #52 opened 3 years ago by pi8027
  1

• Magic number `100%N` used as "fuel" in reflexive normalization (?)

  #57 opened 3 years ago by pi8027
  11

• `ring_simplify`

  #56 opened 3 years ago by pi8027
  0

• A performance issue with morphism detection

  #27 opened 3 years ago by pi8027
  3

• opam package

  #23 opened 3 years ago by amahboubi
  41

• Semi-automating proofs of nonzero conditions in `field`

  #20 opened 3 years ago by pi8027
  2

• Better support for product rings

  #12 opened 4 years ago by pi8027
  0

• Better handling of nonzero conditions in `field`

  #13 opened 3 years ago by pi8027
  2

• Support additive functions and Z-modules

  #14 opened 3 years ago by pi8027
  0

• Support converse rings

  #17 opened 3 years ago by pi8027
  0

• Support ring expressions with exponents

  #11 opened 4 years ago by pi8027
  3

• Performance issue of reflection and support for morphisms

  #4 opened 4 years ago by pi8027
  1

• Move elpi code to a .elpi file

  #6 opened 4 years ago by gares
  0

• Hypothesis handling

  #5 opened 4 years ago by pi8027
  0

• `exact<:` does not check the term is a proof of the current goal

  #1 opened 4 years ago by gares
  4