math-classes

math-classes copied to clipboard

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

2

The Coq team released Coq `8.16+rc1` on June 01, 2022. The corresponding Coq Platform release `2022.09` should be released before **September 15, 2022**. It can be delayed in case of...

MSoegtropIMC

Please suggest example file for Coq Platform "smoke test kit"

1

I just added math-classes to Coq Platform (sorry for the long delay). In Coq Platform we have a so called "smoke test kit", which runs one or two example files...

MSoegtropIMC

Avoid relying on `Add Field` calling `Add Ring`.

5

This is in preparation for https://github.com/coq/coq/pull/10734 Should be backward compatible

maximedenes

RingOrder for types with decidable equality

2

I'm interested in working with ordered rings with decidable equality (in particular, I would like to show that the field of fractions of an ordered ring is also ordered in...

mdgeorge4153

Fix for a new rapply tactic

2

This backwards compatible change makes math-classes work with coq/coq#10760 by replacing all instances of `rapply` which were relying on typeclass resolution happening *before* `refine` (instead of simultaneously with it) to...

JasonGross

spitters

Autogenerate dependency graphs, documentation with travis

1

This can be done as in the https://github.com/HoTT/HoTT @Zimmi48 , does the coq-community has standard template for this? It makes sense to role out this tools uniformly

spitters

Made poly_mult_cr function an instance of ScalarMult and added Module instance.

tymmym

One needs the additional axioms, see #15. ```coq ; in_pos_def1 :> ∀ v, PropHolds (0 ≤ ⟨v,v⟩) ; in_pos_def2 :> ∀ v, 0 = ⟨v,v⟩ v = mon_unit ; inprod_proper...

langston-barrett

I am getting a lot of warnings like these: ```Warning: Notation _ = _ was already used in scope type_scope. [notation-overridden,parsing] Warning: Notation _ ≠ _ was already used in...

vzaliva