Code

Clarify structure#2

Code

Merged

proux01 merged 29 commits intomastercoq/stdlib:masterfrom clarify-structurecoq/stdlib:clarify-structureCopy head branch name to clipboardFeb 3, 2025

+3,539-2,103

Commits

Commits on Feb 1, 2025

• Change -R to -Q

  proux01

  committed
  fc5b1e7

  Copy full SHA for fc5b1e7

• Compile ConstructiveEpsilon without Arith

  proux01

  committed
  e63e953

  Copy full SHA for e63e953

• Compile WeakFan without List

  Show description for 2a1e7a9
  proux01

  committed
  2a1e7a9

  Copy full SHA for 2a1e7a9

• Compile RelationPairs without SetoidList

  proux01

  committed
  42ddd15

  Copy full SHA for 42ddd15

• Compile Classes.SetoidDec without Arith

  proux01

  committed
  fc08da6

  Copy full SHA for fc08da6

• Compile Cantor.v without micromega

  proux01

  committed
  709a5c2

  Copy full SHA for 709a5c2

• Compile Logic/WKL without Arith

  proux01

  committed
  81c39e8

  Copy full SHA for 81c39e8

• Compile NArith without ring

  proux01

  committed
  1500289

  Copy full SHA for 1500289

• Compile ZArith without QArith

  proux01

  committed
  41d957a

  Copy full SHA for 41d957a

• Compile NsatzTactic without QArith

  proux01

  committed
  2f9f490

  Copy full SHA for 2f9f490

• Compile Floats without Psatz

  proux01

  committed
  834cc51

  Copy full SHA for 834cc51

• Compile lists without positive

  proux01

  committed
  3921066

  Copy full SHA for 3921066

• Compile ring without ZArith

  proux01

  committed
  982ce13

  Copy full SHA for 982ce13

• Compile lia without ZArith

  proux01

  committed
  9286b12

  Copy full SHA for 9286b12

• Compile field without QArith

  proux01

  committed
  f26c817

  Copy full SHA for f26c817

• Compile lqa without QArith

  proux01

  committed
  a949a96

  Copy full SHA for a949a96

• Move FinFun and Bvector to Vectors

  proux01

  committed
  71bd08d

  Copy full SHA for 71bd08d

• Move Qreals from QArith to Reals

  proux01

  committed
  7c87329

  Copy full SHA for 7c87329

• Move SetoidList and SetoidPermutation from Lists to Sorting

  proux01

  committed
  7f63588

  Copy full SHA for 7f63588

• Move BoolOrder from Bool to Structures

  proux01

  committed
  6de9b45

  Copy full SHA for 6de9b45

• Move Zerob from Bool to Arith

  proux01

  committed
  9edf8bc

  Copy full SHA for 9edf8bc

• Move Nsatz from nsatz to Reals

  proux01

  committed
  7e10c3d

  Copy full SHA for 7e10c3d

• Move Streams to their own directory

  proux01

  committed
  e0c2a5f

  Copy full SHA for e0c2a5f

• Move MExtraction from micromega to test-suite

  proux01

  committed
  78e3e52

  Copy full SHA for 78e3e52

• [CI] Add a job to check the subcomponent structure

  Show description for bb12522
  proux01

  committed
  bb12522

  Copy full SHA for bb12522

Commits on Feb 2, 2025

• [doc] Add dependency graph

  proux01

  committed
  ee18061

  Copy full SHA for ee18061

• [doc] Better reflect structure

  proux01

  committed
  a0a491e

  Copy full SHA for a0a491e

• [dev-doc] Document the structure checking

  proux01

  committed
  7b452fb

  Copy full SHA for 7b452fb

• [CI] Add a job to check for duplicate files

  Show description for 620b432
  proux01

  committed
  620b432

  Copy full SHA for 620b432