List view

compatibility with coq 8.12

Status: Merged (completed).

math-comp/analysisnumber 241

#241 In math-comp/analysis;

· by affeldt-aist was closed on Jul 27, 2020

minor fix, generalizations, cleaning

Status: Merged (completed).

math-comp/analysisnumber 243

#243 In math-comp/analysis;

· by affeldt-aist was closed on Aug 7, 2020

Generalise properties from pseudo metric to uniform spaces

Status: Merged (completed).

math-comp/analysisnumber 245

#245 In math-comp/analysis;

· by drouhling was closed on Aug 7, 2020

more technical lemmas about extended numbers' arithmetic

Status: Merged (completed).

math-comp/analysisnumber 236

#236 In math-comp/analysis;

· by affeldt-aist was closed on Jul 27, 2020

small theory about arithmetic and geometric sequences

Status: Merged (completed).

math-comp/analysisnumber 239

#239 In math-comp/analysis;

· by affeldt-aist was closed on Jul 28, 2020

Generalize prod_pseudoMetricNormedZmodType

Status: Merged (completed).

math-comp/analysisnumber 232

#232 In math-comp/analysis;

· by pi8027 was closed on Aug 7, 2020

rename "locally" to "nbhs" and propagate

Status: Merged (completed).

math-comp/analysisnumber 233

#233 In math-comp/analysis;

· by affeldt-aist was closed on Jul 27, 2020

minor change to ereal

Status: Merged (completed).

math-comp/analysisnumber 244

#244 In math-comp/analysis;

· by affeldt-aist was closed on Aug 7, 2020

Move stdlib-related code to Rbar/Rstruct

Status: Merged (completed).

math-comp/analysisnumber 246

#246 In math-comp/analysis;

· by drouhling was closed on Aug 7, 2020

Insert a structure of uniform space

Status: Merged (completed).

math-comp/analysisnumber 242

#242 In math-comp/analysis;

· by drouhling was closed on Jul 31, 2020

more lemmas about classical sets

Status: Merged (completed).

math-comp/analysisnumber 240

#240 In math-comp/analysis;

· by affeldt-aist was closed on Jul 27, 2020

contributing file

Status: Merged (completed).

math-comp/analysisnumber 197

#197 In math-comp/analysis;

· by affeldt-aist was closed on Aug 7, 2020

WIP / Experiment : Remove the dependency on R

Status: Closed (abandoned).

math-comp/analysisnumber 112

#112 In math-comp/analysis;

· by drouhling was closed on Aug 8, 2020

Remove this lemma about derivative and replace.

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

experiment 🧪This issue/PR is very experimentalThis issue/PR is very experimental

Status: Closed (completed).

#7 In math-comp/analysis;

· by CohenCyril was closed on Aug 7, 2020

move to boolp

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

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

Status: Closed (completed).

#228 In math-comp/analysis;

· by affeldt-aist was closed on Jul 20, 2020

<code>locally</code> better be renamed after neighborhoods

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

Status: Closed (completed).

#214 In math-comp/analysis;

· by affeldt-aist was closed on Jul 27, 2020