Search results

Typo in rocq doc

Status: Open.

#1965 In math-comp/analysis;

· fblanqui opened on May 12, 2026

Please pick the version you prefer for Rocq 9.1 in Rocq Platform 2026.05

Status: Open.

#1962 In math-comp/analysis;

· Justme0606 opened on May 6, 2026

The norm of a normedModule should be valued in a realType, not in its field of scalar. Definition of subNumDomain.

Status: Open.

#1959 In math-comp/analysis;

· mkerjean opened on May 1, 2026

rename wopen to initial_open

Status: Open.

#1957 In math-comp/analysis;

· affeldt-aist opened on May 1, 2026

·  

1.17.0

FTC statements lack generality and +oo case

Status: Open.

#1956 In math-comp/analysis;

· amolinamounier opened on Apr 28, 2026

fix documentation in set_interval.v

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

Status: Open.

#1942 In math-comp/analysis;

· affeldt-aist opened on Apr 19, 2026

·  

1.17.0

Make pseudometric_normedZmodType depend on topologicalNmodule

Status: Open.

#1935 In math-comp/analysis;

· mkerjean opened on Apr 15, 2026

·  

1.18.0

continuous_linear_bounded should be generalized to convexTvsType

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1927 In math-comp/analysis;

· affeldt-aist opened on Apr 3, 2026

·  

1.17.0

rename sub_sigma_algebra2

Status: Open.

#1923 In math-comp/analysis;

· affeldt-aist opened on Mar 31, 2026

·  

1.17.0

consider making the information r > 0 explicit in open_subball_rat?

question ❓There is an unanswered question hereThere is an unanswered question here

Status: Open.

#1920 In math-comp/analysis;

· affeldt-aist opened on Mar 26, 2026

·  

1.17.0

Vector space with basis

enhancement ✨This issue/PR is about adding new features enhancing the libraryThis issue/PR is about adding new features enhancing the library

Status: Open.

#1911 In math-comp/analysis;

· Tragicus opened on Mar 19, 2026

·  

1.17.0

packager: coq -> rocq

packaging/releasingIssue/PR about packaging or realising.Issue/PR about packaging or realising.

Status: Open.

#1905 In math-comp/analysis;

· affeldt-aist opened on Mar 16, 2026

·  

1.17.0