Search results

CI failures when MathComp dev version is picked up

Status: Open.

#2006 In math-comp/analysis;

· yoshihiro503 opened on Jun 24, 2026

Allow for Rocq 9.2 in opam files

Status: Open.

#2002 In math-comp/analysis;

· affeldt-aist opened on Jun 18, 2026

is_diff is not documented in the header

documentation 📝This issue/PR is about documentation of the library / repositoryThis issue/PR is about documentation of the library / repository

Status: Open.

#1996 In math-comp/analysis;

· affeldt-aist opened on Jun 12, 2026

·  

1.18.0

PseudoMetricNormedZmodules should inherit from MetricType

Status: Open.

#1995 In math-comp/analysis;

· Brixfoly opened on Jun 11, 2026

Shoulnd't nbhs_dnbhs_neq be a Hint?

Status: Open.

#1994 In math-comp/analysis;

· affeldt-aist opened on Jun 11, 2026

·  

1.18.0

Define filter comap

Status: Open.

#1991 In math-comp/analysis;

· mkerjean opened on Jun 9, 2026

TODO: rename pseudometric

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1990 In math-comp/analysis;

· affeldt-aist opened on Jun 9, 2026

·  

1.18.0

Add posnum instances for ratio lemmas

Status: Open.

#1989 In math-comp/analysis;

· mkerjean opened on Jun 9, 2026

measure space is likely to be needed

Status: Open.

#1985 In math-comp/analysis;

· t6s opened on Jun 3, 2026

nbhs basis in tvs.v

Status: Open.

#1981 In math-comp/analysis;

· mkerjean opened on May 29, 2026

_subproof prefixes

renaming/refactoring 🔧This is about a renaming or refactoring in the libraryThis is about a renaming or refactoring in the library

Status: Open.

#1980 In math-comp/analysis;

· affeldt-aist opened on May 29, 2026

Conflicting |_| and Norm/SemiNorm notations

Status: Open.

#1976 In math-comp/analysis;

· mkerjean opened on May 18, 2026