Code

Adding a CEP about Reals#74

Code

Open

Villetaneuse wants to merge 3 commits intocoq:mastercoq/rfcs:masterfrom Villetaneuse:clean_up_RealsVilletaneuse/ceps:clean_up_RealsCopy head branch name to clipboard

+136

Commits

Commits on Sep 15, 2023

• Adding a CEP about Reals

  Villetaneuse

  committed
  4240d3b

  Copy full SHA for 4240d3b

Commits on Sep 18, 2023

• Mention mathcomp-analysis and C-Corn

  Villetaneuse

  committed
  2caa44c

  Copy full SHA for 2caa44c

Commits on Sep 29, 2023

• Correct statements about math-comp/analysis

  Show description for 2cc502a
  Villetaneuse

  committed
  2cc502a

  Copy full SHA for 2cc502a