Skip to content

ORIGINAL_FILES.md

Latest commit

 

History

History
37 lines (31 loc) · 1.2 KB

ORIGINAL_FILES.md

File metadata and controls

37 lines (31 loc) · 1.2 KB

Origins of the files in this repository

This description corresponds to the first releases.

Original files from this library

  • posnum.v
  • classical_set.v
  • topology.v (with uniform space (now renamed pseudo metric space) and complete space inspired from Coquelicot's hierarchy.v)
  • normedtype.v (with normed and complete normed spaces inspired from Coquelicot's hierarchy.v)
  • landau.v
  • derive.v
  • README.md
  • AUTHORS.md
  • FILES.md
  • INSTALL.md
  • _CoqProject
  • Makefile
  • Licence_CeCILL-C_V1-en.txt

Files from the former library coq-alternate-reals are now here and should be merged at some point:

  • boolp.v
  • dedekind.v
  • discrete.v
  • distr.v
  • reals.v
  • realseq.v
  • realsum.v
  • xfinmap.v
  • xsets.v

Files modified from Coquelicot 3.0.1

  • Rbar.v (now removed in favor of ereal.v)

Other files

  • Rstruct.v from CoqApprox, with contributions from Sophie Bernard, from her repository (https://github.com/Sobernard/Struct/blob/master/Rstruct.v), and modified to instantiate structures from coq-alternate-reals.
  • forms.v by Cyril Cohen and Laurence Rideau, temporarily added to this repository until it is merged in the Mathematical Components library