List view

semi_additive is also defined in MathComp 2

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

Status: Closed (completed).

#1072 In math-comp/analysis;

· by affeldt-aist was closed on Feb 24, 2026

Renaming weak topology as initial topology

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

Status: Closed (completed).

#1570 In math-comp/analysis;

· by mkerjean was closed on Feb 8, 2026

itv_is_ray

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

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

Status: Closed (completed).

#1823 In math-comp/analysis;

· by affeldt-aist was closed on Jan 17, 2026

[CI] Add infotheo

Status: Merged (completed).

math-comp/analysisnumber 1826

#1826 In math-comp/analysis;

· by proux01 was closed on Jan 16, 2026

rename and boolify some predicates for open intervals

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

Status: Merged (completed).

math-comp/analysisnumber 1825

#1825 In math-comp/analysis;

· by t6s was closed on Jan 17, 2026

Allow rocq 9.1

build/continuous integration ⚙️This issue/PR is about the build process or CIThis issue/PR is about the build process or CI

Status: Merged (completed).

math-comp/analysisnumber 1832

#1832 In math-comp/analysis;

· by garrigue was closed on Feb 2, 2026

better behaved Rintegral_cst

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Merged (completed).

math-comp/analysisnumber 1833

#1833 In math-comp/analysis;

· by affeldt-aist was closed on Feb 3, 2026

rename weak_topology -> initial_topology

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

Status: Merged (completed).

math-comp/analysisnumber 1834

#1834 In math-comp/analysis;

· by affeldt-aist was closed on Feb 8, 2026

Doc: make html display the tag name instead of the commit hash.

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

Status: Merged (completed).

math-comp/analysisnumber 1835

#1835 In math-comp/analysis;

· by yoshihiro503 was closed on Feb 5, 2026

fix itv_closed_ends

"bug" 🐛This issue (resp. PR) describes (resp. fixes) a "bug"This issue (resp. PR) describes (resp. fixes) a "bug"

Status: Merged (completed).

math-comp/analysisnumber 1838

#1838 In math-comp/analysis;

· by t6s was closed on Feb 5, 2026

usefulness of in_set1

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

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

Status: Closed (completed).

#1841 In math-comp/analysis;

· by affeldt-aist was closed on Feb 24, 2026

split probability.v

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

Status: Merged (completed).

math-comp/analysisnumber 1842

#1842 In math-comp/analysis;

· by affeldt-aist was closed on Feb 11, 2026

naming of closed_comp

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

Status: Closed (completed).

#1843 In math-comp/analysis;

· by affeldt-aist was closed on Feb 25, 2026

TODO: try to move function_spaces to topology_theory

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

Status: Closed (completed).

#1844 In math-comp/analysis;

· by affeldt-aist was closed on Mar 6, 2026

TODO: check whether we can use apply:

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

Status: Closed (completed).

#1845 In math-comp/analysis;

· by affeldt-aist was closed on Feb 22, 2026

put convex.v lower in the file hier

Status: Merged (completed).

math-comp/analysisnumber 1850

#1850 In math-comp/analysis;

· by affeldt-aist was closed on Feb 19, 2026

Adapt to https://github.com/rocq-prover/rocq/pull/21611

Status: Merged (completed).

math-comp/analysisnumber 1851

#1851 In math-comp/analysis;

· by proux01 was closed on Feb 18, 2026

fixes #1845

Status: Merged (completed).

math-comp/analysisnumber 1854

#1854 In math-comp/analysis;

· by affeldt-aist was closed on Feb 22, 2026

naming glitch at closure_subset

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

Status: Closed (completed).

#1849 In math-comp/analysis;

· by t6s was closed on Feb 25, 2026

fix #1843

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

Status: Merged (completed).

math-comp/analysisnumber 1855

#1855 In math-comp/analysis;

· by affeldt-aist was closed on Feb 25, 2026

fix #1841

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

Status: Merged (completed).

math-comp/analysisnumber 1856

#1856 In math-comp/analysis;

· by affeldt-aist was closed on Feb 24, 2026

derive_mx

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

Status: Merged (completed).

math-comp/analysisnumber 1829

#1829 In math-comp/analysis;

· by affeldt-aist was closed on Mar 9, 2026

forgotten closing tactical?

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

Status: Closed (completed).

#1858 In math-comp/analysis;

· by affeldt-aist was closed on Mar 2, 2026

lemmas about within-continuity

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

Status: Merged (completed).

math-comp/analysisnumber 1859

#1859 In math-comp/analysis;

· by affeldt-aist was closed on Feb 27, 2026

would it make sense to use the predicate setI_closed here?

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

Status: Closed (completed).

#1863 In math-comp/analysis;

· by affeldt-aist was closed on Mar 3, 2026