Code

Clarify structure#2

Code

Open

proux01 wants to merge 181 commits intomastercoq/stdlib:masterfrom clarify-structurecoq/stdlib:clarify-structureCopy head branch name to clipboard

+20,289-593,112

Commits

Commits on Oct 24, 2024

• Warn when missing "From Stdlib" in Require

  proux01

  committed
  4bfa772

  Copy full SHA for 4bfa772

• Add Bool.Sumbool to prelude

  proux01

  committed
  4a416fb

  Copy full SHA for 4a416fb

• Add reflect to Init

  proux01

  committed
  8bc1a73

  Copy full SHA for 8bc1a73

• Remove dependency of ssr on Bool

  proux01

  committed
  193840a

  Copy full SHA for 193840a

• Remove dependencies on Extraction and FunExt

  proux01

  committed
  b39ef29

  Copy full SHA for b39ef29

• Restrict dependencies of axioms specifying primitive operators

  proux01

  committed
  e3d15da

  Copy full SHA for e3d15da

• [test-suite] Split tests requiring Arith

  proux01

  committed
  2ce0977

  Copy full SHA for 2ce0977

• [test-suite] Split tests requiring ZArith

  proux01

  committed
  93735d1

  Copy full SHA for 93735d1

• [test-suite] Split tests requiring String

  proux01

  committed
  9ca9418

  Copy full SHA for 9ca9418

• [test-suite] Split test requiring Lia

  proux01

  committed
  e125ee2

  Copy full SHA for e125ee2

• [test-suite] Cleanup some stdlib dependencies

  proux01

  committed
  e11a43c

  Copy full SHA for e11a43c

• [test-suite] Cleanup dependency on stdlib in ssr

  proux01

  committed
  ea38df5

  Copy full SHA for ea38df5

• [test-suite] Cleanup dependencies in primitive/arrays

  proux01

  committed
  22091d8

  Copy full SHA for 22091d8

• [test-suite] Cleanup dependencies in primitive/float

  proux01

  committed
  8648dbe

  Copy full SHA for 8648dbe

• [test-suite] Cleanup dependencies in primitive/string

  proux01

  committed
  5a8e17a

  Copy full SHA for 5a8e17a

• [test-suite] Cleanup dependencies in primitive/int63

  proux01

  committed
  ad1e1bc

  Copy full SHA for ad1e1bc

• [test-suite] Cleanup dependencies on Arith

  proux01

  committed
  1c29f94

  Copy full SHA for 1c29f94

• [test-suite] Cleanup dependency on Extraction

  proux01

  committed
  81f3771

  Copy full SHA for 81f3771

• [test-suite] Cleanup dependency in Floats

  proux01

  committed
  6189fba

  Copy full SHA for 6189fba

• [test-suite] Cleanup dependencies on List

  proux01

  committed
  a74847e

  Copy full SHA for a74847e

• [test-suite] Cleanup dependencies on NArith

  proux01

  committed
  a72d3f2

  Copy full SHA for a72d3f2

• [test-suite] Cleanup dependency on PArray

  proux01

  committed
  5b1f0f6

  Copy full SHA for 5b1f0f6

• [test-suite] Cleanup dependencies on PArith

  proux01

  committed
  c4c96d0

  Copy full SHA for c4c96d0

• [test-suite] Cleanup dependencies on Program

  proux01

  committed
  3edd85e

  Copy full SHA for 3edd85e

• [test-suite] Cleanup dependency on RelationClasses

  proux01

  committed
  523f76d

  Copy full SHA for 523f76d

• [test-suite] Cleanup dependency on Relations

  proux01

  committed
  40faafb

  Copy full SHA for 40faafb

• [test-suite] Cleanup dependencies on String

  proux01

  committed
  6d0647b

  Copy full SHA for 6d0647b

• [test-suite] Cleanup dependencies on Uint63

  proux01

  committed
  77b7cb0

  Copy full SHA for 77b7cb0

• [test-suite] Cleanup dependencies on Utf8

  proux01

  committed
  3ff4352

  Copy full SHA for 3ff4352

• [test-suite] Cleanup dependencies on ZArith

  proux01

  committed
  9d1e7b4

  Copy full SHA for 9d1e7b4

• [test-suite] Cleanup dependeny on Bool

  proux01

  committed
  c743f35

  Copy full SHA for c743f35

• [test-suite] Cleanup dependency on FunExt

  proux01

  committed
  5d366aa

  Copy full SHA for 5d366aa

• [test-suite] Cleanup dependencies on FunInd

  proux01

  committed
  6775684

  Copy full SHA for 6775684

• [test-suite] Cleanup dependencies on Hurkens

  proux01

  committed
  bc92487

  Copy full SHA for bc92487

• [test-suite] Cleanup dependency on JMeq

  proux01

  committed
  fe09292

  Copy full SHA for fe09292

• [test-suite] Move tests requiring Arith

  proux01

  committed
  f104bd6

  Copy full SHA for f104bd6

• [test-suite] Move test requiring Bool

  proux01

  committed
  0ee05f8

  Copy full SHA for 0ee05f8

• [test-suite] Move tests requiring btauto

  proux01

  committed
  95ad293

  Copy full SHA for 95ad293

• [test-suite] Move test requiring CEquivalence

  proux01

  committed
  13f1f26

  Copy full SHA for 13f1f26

• [test-suite] Move test requiring Classes.Equivalence

  proux01

  committed
  3cd364b

  Copy full SHA for 3cd364b

• [test-suite] Move test requiring Classical

  proux01

  committed
  9a1b05c

  Copy full SHA for 9a1b05c

• [test-suite] Move test requiring Classical_prop

  proux01

  committed
  e1b482e

  Copy full SHA for e1b482e

• [test-suite] Move test requiring Cyclic

  proux01

  committed
  3b09203

  Copy full SHA for 3b09203

• [test-suite] Move test requiring DecidableClasses

  proux01

  committed
  578e30c

  Copy full SHA for 578e30c

• [test-suite] Move tests requiring Ensembles

  proux01

  committed
  6cbc0cd

  Copy full SHA for 6cbc0cd

• [test-suite] Move tests requiring Eqdep

  proux01

  committed
  357a331

  Copy full SHA for 357a331

• [test-suite] Move tests requiring Equality

  proux01

  committed
  912aea1

  Copy full SHA for 912aea1

• [test-suite] Move tests requiring EquivDec

  proux01

  committed
  2de51c3

  Copy full SHA for 2de51c3

• [test-suite] Move test requiring field

  proux01

  committed
  b613db7

  Copy full SHA for b613db7

• [test-suite] Move test requiring Floats

  proux01

  committed
  ee17daa

  Copy full SHA for ee17daa

• [test-suite] Move tests requiring FSets

  proux01

  committed
  51115c1

  Copy full SHA for 51115c1

• [test-suite] Move test requiring FunExt

  proux01

  committed
  7f99d33

  Copy full SHA for 7f99d33

• [test-suite] Move test requiring FunInd

  proux01

  committed
  79fa153

  Copy full SHA for 79fa153

• [test-suite] Move test requiring JMeq

  proux01

  committed
  6a9b3de

  Copy full SHA for 6a9b3de

• [test-suite] Move tests requiring Lia

  proux01

  committed
  0d0cc60

  Copy full SHA for 0d0cc60

• [test-suite] Move tests requiring List

  proux01

  committed
  7aed9ce

  Copy full SHA for 7aed9ce

• [test-suite] Move tests requiring Logic.Eqnotations

  proux01

  committed
  bb7c9f4

  Copy full SHA for bb7c9f4

• [test-suite] Move test requiring Lra

  proux01

  committed
  803045d

  Copy full SHA for 803045d

• [test-suite] Move tests requiring micromega

  proux01

  committed
  196e784

  Copy full SHA for 196e784

• [test-suite] Move tests requiring MSet

  proux01

  committed
  81df4cb

  Copy full SHA for 81df4cb

• [test-suite] Move tests requiring NArith

  proux01

  committed
  a60229c

  Copy full SHA for a60229c

• [test-suite] Move tests requiring Nsatz

  proux01

  committed
  594dee8

  Copy full SHA for 594dee8

• [test-suite] Move tests requiring OrderEx

  proux01

  committed
  7b7a7b8

  Copy full SHA for 7b7a7b8

• [test-suite] Move test requiring PArith

  proux01

  committed
  37bcd5b

  Copy full SHA for 37bcd5b

• [test-suite] Move test requiring PeanoNat

  proux01

  committed
  ca79e0c

  Copy full SHA for ca79e0c

• [test-suite] Move tests requiring Program

  proux01

  committed
  bde082b

  Copy full SHA for bde082b

• [test-suite] Move tests requiring Program.Equality

  proux01

  committed
  2f66d6f

  Copy full SHA for 2f66d6f

• [test-suite] Move tests requiring Psatz

  proux01

  committed
  3354eb2

  Copy full SHA for 3354eb2

• [test-suite] Move tests requiring QArith

  proux01

  committed
  04261e3

  Copy full SHA for 04261e3

• [test-suite] Move tests requiring Reals

  proux01

  committed
  ead88b4

  Copy full SHA for ead88b4

• [test-suite] Move tests requiring ring

  proux01

  committed
  d08cb13

  Copy full SHA for d08cb13

• [test-suite] Move tests requiring SetoidClass

  proux01

  committed
  78425ee

  Copy full SHA for 78425ee

• [test-suite] Move tests requiring SetoidList

  proux01

  committed
  b0f80b0

  Copy full SHA for b0f80b0

• [test-suite] Move tests requiring Sint63

  proux01

  committed
  a71c19b

  Copy full SHA for a71c19b

• [test-suite] Move tests requiring String

  proux01

  committed
  ae3a4af

  Copy full SHA for ae3a4af

• [test-suite] Move tests requiring Utf8

  proux01

  committed
  f2439ea

  Copy full SHA for f2439ea

• [test-suite] Move tests requiring Vector

  proux01

  committed
  de271cd

  Copy full SHA for de271cd

• [test-suite] Move test requiring Wf_nat

  proux01

  committed
  ea086f5

  Copy full SHA for ea086f5

• [test-suite] Move tests requiring ZArith

  proux01

  committed
  f23f27c

  Copy full SHA for f23f27c

• Move stdlib

  proux01

  committed
  c3d483a

  Copy full SHA for c3d483a

• [test-suite] Fix misc test after removing stdlib

  proux01

  committed
  8004347

  Copy full SHA for 8004347

• [stdlib] Adapt README.md and INSTALL.md

  proux01

  committed
  ae167a5

  Copy full SHA for ae167a5

• [stdlib] Add a basic Makefile to compile everything

  proux01

  committed
  9fbc2f2

  Copy full SHA for 9fbc2f2

• [stdlib] Adapt Compat

  proux01

  committed
  718f377

  Copy full SHA for 718f377

• [stdlib] Adapt test-suite

  proux01

  committed
  abd2209

  Copy full SHA for abd2209

• [stdlib] Compile refman

  proux01

  committed
  a475676

  Copy full SHA for a475676

• [stdlib] Compile html doc

  proux01

  committed
  9d4da58

  Copy full SHA for 9d4da58

• [refman] Add an 'extra' option to '.. coqtop::'

  Show description for 2a7c4dd
  proux01

  committed
  2a7c4dd

  Copy full SHA for 2a7c4dd

• [refman] Compile the refman mostly without stdlib

  Show description for 1be72b5
  proux01

  committed
  1be72b5

  Copy full SHA for 1be72b5

• Compile prelude doc without stdlib

  proux01

  committed
  804276c

  Copy full SHA for 804276c

• Update CONTRIBUTING.md

  proux01

  committed
  a8d0ed4

  Copy full SHA for a8d0ed4

• Rename OPAM package coq-stdlib -> rocq-init

  proux01

  committed
  7d910a7

  Copy full SHA for 7d910a7

• [CI] Add stdlib

  proux01

  committed
  19efd8e

  Copy full SHA for 19efd8e

• [CI] Add refman with all extras

  proux01

  committed
  388389b

  Copy full SHA for 388389b

• Add overlays

  proux01

  committed
  de2f1be

  Copy full SHA for de2f1be

• Add changelog

  proux01

  committed
  37883e1

  Copy full SHA for 37883e1

• Keep a few files in stdlib

  proux01

  committed
  a187b32

  Copy full SHA for a187b32

• Remove all but stdlib

  proux01

  committed
  f2a701d

  Copy full SHA for f2a701d

• Move stdlib

  proux01

  committed
  3805e70

  Copy full SHA for 3805e70

• Adapt changelog

  proux01

  committed
  5f43cea

  Copy full SHA for 5f43cea

• Adapt CONTRIBUTING.md

  proux01

  committed
  4e4f33a

  Copy full SHA for 4e4f33a

• Update Pull Request template

  proux01

  committed
  5905e92

  Copy full SHA for 5905e92

• Adapt CI

  Show description for 1143e06
  proux01

  committed
  1143e06

  Copy full SHA for 1143e06

• [CI] Add a job to run test-suite

  Show description for 472b1cd
  

  proux01

  and

  CohenCyril

  committed
  472b1cd

  Copy full SHA for 472b1cd

• [CI] Add a job refman-html

  Show description for c21e702
  

  proux01

  and

  CohenCyril

  committed
  c21e702

  Copy full SHA for c21e702

• [CI] Add a job stdlib-html

  Show description for e41231a
  

  proux01

  and

  CohenCyril

  committed
  e41231a

  Copy full SHA for e41231a

• [CI] Retrieve lint job

  proux01

  committed
  f67bccd

  Copy full SHA for f67bccd

• [CI] Add a README

  proux01

  committed
  7996192

  Copy full SHA for 7996192

• Change -R to -Q

  proux01

  committed
  3d7797b

  Copy full SHA for 3d7797b

• Compile ConstructiveEpsilon without Arith

  proux01

  committed
  1937a98

  Copy full SHA for 1937a98

• Compile WeakFan without List

  Show description for fb0e7e8
  proux01

  committed
  fb0e7e8

  Copy full SHA for fb0e7e8

• Compile RelationPairs without SetoidList

  proux01

  committed
  aa83e9c

  Copy full SHA for aa83e9c

• Compile Classes.SetoidDec without Arith

  proux01

  committed
  2572ef6

  Copy full SHA for 2572ef6

• Compile Cantor.v without micromega

  proux01

  committed
  0548c93

  Copy full SHA for 0548c93

• Compile Logic/WKL without Arith

  proux01

  committed
  313b1c1

  Copy full SHA for 313b1c1

• Compile NArith without ring

  proux01

  committed
  347a72e

  Copy full SHA for 347a72e

• Compile ZArith without QArith

  proux01

  committed
  d0efd3b

  Copy full SHA for d0efd3b

• Compile NsatzTactic without QArith

  proux01

  committed
  b2b4ade

  Copy full SHA for b2b4ade

• Compile Floats without Psatz

  proux01

  committed
  6baf90f

  Copy full SHA for 6baf90f

• Compile lists without positive

  proux01

  committed
  3e32e1c

  Copy full SHA for 3e32e1c

• Move FinFun and Bvector to Vectors

  proux01

  committed
  900530e

  Copy full SHA for 900530e

• Move Qreals from QArith to Reals

  proux01

  committed
  2149b44

  Copy full SHA for 2149b44

• Move SetoidList and SetoidPermutation from Lists to Sorting

  proux01

  committed
  9f8fff8

  Copy full SHA for 9f8fff8

• Move BoolOrder from Bool to Structures

  proux01

  committed
  af41e27

  Copy full SHA for af41e27

• Move Zerob from Bool to Arith

  proux01

  committed
  c60abbd

  Copy full SHA for c60abbd

• Move Nsatz from nsatz to Reals

  proux01

  committed
  99730b3

  Copy full SHA for 99730b3

• Move Streams to their own directory

  proux01

  committed
  ab77ab4

  Copy full SHA for ab77ab4

• Move MExtraction from micromega to test-suite

  proux01

  committed
  16ea617

  Copy full SHA for 16ea617

• Detail _CoqProject

  proux01

  committed
  3ebbf05

  Copy full SHA for 3ebbf05

• Split Logic into subdirectories Base, Classical and Lists

  proux01

  committed
  dfbc314

  Copy full SHA for dfbc314

• Split Classes into subdirectories All, Arith and Lists

  proux01

  committed
  a13f5d9

  Copy full SHA for a13f5d9

• Split Numbers into subdirectories Arith, List, positive, Z, Q, R and Strings

  proux01

  committed
  101be70

  Copy full SHA for 101be70

• Split Structures into subdirectories Def and Ex

  proux01

  committed
  33ca66c

  Copy full SHA for 33ca66c

• Split Arith into subdirectories All and Base

  proux01

  committed
  bda196b

  Copy full SHA for bda196b

• Split ZArith into subdirectories All, Base and Ring

  proux01

  committed
  dd31bb8

  Copy full SHA for dd31bb8

• Split QArith into subdirectories All, Base and Field

  proux01

  committed
  c73719b

  Copy full SHA for c73719b

• Split setoid_ring into subdirectories Q, R and Z

  proux01

  committed
  3529e60

  Copy full SHA for 3529e60

• Split micromega into subdirectories Int63, Lia, Lqa, Lra and Zify

  proux01

  committed
  566c65f

  Copy full SHA for 566c65f

• Add dependency graph

  proux01

  committed
  bfc8e8b

  Copy full SHA for bfc8e8b

• Add Makefile for logic

  proux01

  committed
  7c62bbd

  Copy full SHA for 7c62bbd

• Add Makefile for streams

  proux01

  committed
  f0fe484

  Copy full SHA for f0fe484

• Add Makefile for program

  proux01

  committed
  bd3f761

  Copy full SHA for bd3f761

• Add Makefile for Relations

  proux01

  committed
  d278bec

  Copy full SHA for d278bec

• Add Makefile for classes

  proux01

  committed
  5dd074e

  Copy full SHA for 5dd074e

• Add Makefile for bool

  proux01

  committed
  d876d38

  Copy full SHA for d876d38

• Add Makefile for structures

  proux01

  committed
  cf4573b

  Copy full SHA for cf4573b

• Add Makefile for arith-base

  proux01

  committed
  f53cbc6

  Copy full SHA for f53cbc6

• Add Makefile for list

  proux01

  committed
  c50168a

  Copy full SHA for c50168a

• Add Makefile for positive

  proux01

  committed
  8bb83c1

  Copy full SHA for 8bb83c1

• Add Makefile for narith

  proux01

  committed
  de589c4

  Copy full SHA for de589c4

• Add Makefile for zarith-base

  proux01

  committed
  6025d3d

  Copy full SHA for 6025d3d

• Add Makefile for ring

  proux01

  committed
  1f134a5

  Copy full SHA for 1f134a5

• Add Makefile for arith

  proux01

  committed
  1e9ff84

  Copy full SHA for 1e9ff84

• Add Makefile for lia

  proux01

  committed
  0ad504e

  Copy full SHA for 0ad504e

• Add Makefile for zarith

  proux01

  committed
  220b355

  Copy full SHA for 220b355

• Add Makefile for unicode

  proux01

  committed
  3127926

  Copy full SHA for 3127926

• Add Makefile for primitive-int

  proux01

  committed
  32bd2ec

  Copy full SHA for 32bd2ec

• Add Makefile for primitive-array

  proux01

  committed
  598d49e

  Copy full SHA for 598d49e

• Add Makefile for vectors

  proux01

  committed
  18e1d06

  Copy full SHA for 18e1d06

• Add Makefile for string

  proux01

  committed
  1a4b542

  Copy full SHA for 1a4b542

• Add Makefile for classical-logic

  proux01

  committed
  ffc24db

  Copy full SHA for ffc24db

• Add Makefile for sets

  proux01

  committed
  50ee031

  Copy full SHA for 50ee031

• Add Makefile for sorting

  proux01

  committed
  776d671

  Copy full SHA for 776d671

• Add Makefile for orders-ex

  proux01

  committed
  9b351d8

  Copy full SHA for 9b351d8

• Add Makefile for primitive-string

  proux01

  committed
  f2458a2

  Copy full SHA for f2458a2

• Add Makefile for primitive-floats

  proux01

  committed
  f195fff

  Copy full SHA for f195fff

• Add Makefile for extraction

  proux01

  committed
  2dfd138

  Copy full SHA for 2dfd138

• Add Makefile for funind

  proux01

  committed
  a0a475a

  Copy full SHA for a0a475a

• Add Makefile for qarith-base

  proux01

  committed
  a61e48c

  Copy full SHA for a61e48c

• Add Makefile for field

  proux01

  committed
  d550745

  Copy full SHA for d550745

• Add Makefile for lqa

  proux01

  committed
  42088ff

  Copy full SHA for 42088ff

• Add Makefile for qarith

  proux01

  committed
  cb5ad72

  Copy full SHA for cb5ad72

• Add Makefile for nsatz

  proux01

  committed
  cc9f571

  Copy full SHA for cc9f571

• Add Makefile for reals

  proux01

  committed
  8de036d

  Copy full SHA for 8de036d

• Add Makefile for fmaps-fsets-msets

  proux01

  committed
  996b465

  Copy full SHA for 996b465

• Add Makefile for wellfounded

  proux01

  committed
  5d14867

  Copy full SHA for 5d14867

• Add Makefile for rtauto

  proux01

  committed
  856b92e

  Copy full SHA for 856b92e

• Add Makefile for compat

  proux01

  committed
  b915bfe

  Copy full SHA for b915bfe

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

  Show description for 91fe0f1
  proux01

  committed
  91fe0f1

  Copy full SHA for 91fe0f1

• [CI] Add a job to check makefiles

  Show description for 47c9ec5
  proux01

  committed
  47c9ec5

  Copy full SHA for 47c9ec5

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

  Show description for e37e2ff
  proux01

  committed
  e37e2ff

  Copy full SHA for e37e2ff