Sitelet https://github.com/math-comp/analysis/commits/master/analysis_stdlib

Commits

History for

Commits on Sep 28, 2026

Compile with +level-tolerance (#2108)
proux01
authored
86b80ee

Commits on Sep 25, 2026

Cleanup old COQ variables in Makefiles (#2111)
proux01
authored
374700f

Commits on Aug 18, 2026

add compatibility lemmas for Stdlib `Rcos` and `Rsin` (#2083)
t6s
authored
7f7f74e

Commits on Jul 29, 2026

Remove all_ssreflect_compat
proux01
committed
e1a47f7

Commits on Apr 3, 2026

Adapt to https://github.com/rocq-prover/rocq/pull/21851
proux01
committed
092644f

Commits on Apr 2, 2026

Silence the new rewrite-rw warning
proux01
committed
cd3de06

Commits on Mar 27, 2026

Port analysis-stdlib to new rewrite goals order
proux01
committed
191c613

Commits on Mar 4, 2026

Forgotten when dropping support for 8.20
proux01
committed
1f27e7a

Commits on Mar 3, 2026

Adapt to https://github.com/math-comp/math-comp/pull/1545 (#1860)
proux01
authored
3ee2f0f

Commits on Feb 20, 2026

Add compat file for all_ssreflect
proux01
committed
641fa46

Commits on Feb 7, 2026

Add a RealsE multirule (#1836)

proux01
and
t6s
authored
e2db34a

Commits on Jan 28, 2026

Added lemma to swap mathcomp natural log with Rocqs natural log (#1831)
lstrsrmn
authored
5e3fad2

Commits on Nov 19, 2025

Cleanup (#1763)
pi8027
authored
096ff50

Commits on Jun 27, 2025

adapt to rocq-prover/rocq#20707 (#1641)
gares
authored
ecc270f

Commits on Mar 14, 2025

equivalence between exponential funcitons in stdlib and mca (#1525)

t6s
and
affeldt-aist
authored
35bcc63

Commits on Feb 19, 2025

Port from signed to itv

committed
9863f51

Commits on Jan 31, 2025

minor generalization (#1461)

affeldt-aist
and
t6s
authored
8a3d671

Commits on Dec 7, 2024

Remove the use of [the _ of _] notations (#1430)
pi8027
authored
cd3d1af

Commits on Oct 28, 2024

Add a coq-mathcomp-reals package

proux01
authored and
affeldt-aist
committed
02ebce5

Loading