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 continuousFunType?

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

Status: Closed (completed).

#1811 In math-comp/analysis;

· by affeldt-aist was closed on Mar 16, 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

Missing canonical declaration in topology.v?

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

Status: Closed (completed).

#154 In math-comp/analysis;

· by amahboubi was closed on Mar 11, 2026

use of deprecated options of Rocqnavi to generate the documentation

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

Status: Closed (completed).

#1749 In math-comp/analysis;

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

Added differentiability of the max function

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 1819

#1819 In math-comp/analysis;

· by lstrsrmn was closed on Mar 12, 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