Give Stdlib its own directory - #19530

Merged

coqbot-app[bot] merged 98 commits into

rocq-prover:masterfrom

proux01:stdlib_repo

Dec 6, 2024

Commits on Dec 5, 2024

Warn when missing "From Stdlib" in Require
proux01
committed
554bfb0
Add Bool.Sumbool to prelude
proux01
committed
4fcdb38
Add reflect to Init
proux01
committed
a9dad25
Remove dependency of ssr on Bool
proux01
committed
1375e16
Remove dependencies on Extraction and FunExt
proux01
committed
e036de5
Restrict dependencies of axioms specifying primitive operators
proux01
committed
91397f6
[test-suite] Split tests requiring Arith
proux01
committed
d91d70a
[test-suite] Split tests requiring ZArith
proux01
committed
bbdd343
[test-suite] Split tests requiring String
proux01
committed
5abc009
[test-suite] Split test requiring Lia
proux01
committed
060c105
[test-suite] Cleanup some stdlib dependencies
proux01
committed
7a5d532
[test-suite] Cleanup dependency on stdlib in ssr
proux01
committed
ebe179a
[test-suite] Cleanup dependencies in primitive/arrays
proux01
committed
755d32a
[test-suite] Cleanup dependencies in primitive/float
proux01
committed
398504a
[test-suite] Cleanup dependencies in primitive/string
proux01
committed
f3e59af
[test-suite] Cleanup dependencies in primitive/int63
proux01
committed
be381ed
[test-suite] Cleanup dependencies on Arith
proux01
committed
f9884a5
[test-suite] Cleanup dependency on Extraction
proux01
committed
20e6b36
[test-suite] Cleanup dependency in Floats
proux01
committed
87696a9
[test-suite] Cleanup dependencies on List
proux01
committed
a460c2b
[test-suite] Cleanup dependencies on NArith
proux01
committed
43c659d
[test-suite] Cleanup dependency on PArray
proux01
committed
d1432d9
[test-suite] Cleanup dependencies on PArith
proux01
committed
4cb738a
[test-suite] Cleanup dependencies on Program
proux01
committed
bb765bc
[test-suite] Cleanup dependency on RelationClasses
proux01
committed
8e8087f
[test-suite] Cleanup dependency on Relations
proux01
committed
32262a9
[test-suite] Cleanup dependencies on String
proux01
committed
96efaec
[test-suite] Cleanup dependencies on Uint63
proux01
committed
1d39418
[test-suite] Cleanup dependencies on Utf8
proux01
committed
2abf2fe
[test-suite] Cleanup dependencies on ZArith
proux01
committed
c5c828d
[test-suite] Cleanup dependeny on Bool
proux01
committed
d3cf171
[test-suite] Cleanup dependency on FunExt
proux01
committed
9ac0222
[test-suite] Cleanup dependencies on FunInd
proux01
committed
4bd4d52
[test-suite] Cleanup dependencies on Hurkens
proux01
committed
2224126
[test-suite] Cleanup dependency on JMeq
proux01
committed
67644c7
[test-suite] Move tests requiring Arith
proux01
committed
d263a85
[test-suite] Move test requiring Bool
proux01
committed
1f155c1
[test-suite] Move tests requiring btauto
proux01
committed
fe2e02b
[test-suite] Move test requiring CEquivalence
proux01
committed
af5894a
[test-suite] Move test requiring Classes.Equivalence
proux01
committed
6d67f0a
[test-suite] Move test requiring Classical
proux01
committed
cb53430
[test-suite] Move test requiring Classical_prop
proux01
committed
92fba28
[test-suite] Move test requiring Cyclic
proux01
committed
fcdd4e4
[test-suite] Move test requiring DecidableClasses
proux01
committed
b77a007
[test-suite] Move tests requiring Ensembles
proux01
committed
f811523
[test-suite] Move tests requiring Eqdep
proux01
committed
e7a5811
[test-suite] Move tests requiring Equality
proux01
committed
62af4e1
[test-suite] Move tests requiring EquivDec
proux01
committed
cfc57e2
[test-suite] Move test requiring field
proux01
committed
d67e332
[test-suite] Move test requiring Floats
proux01
committed
857e6c8
[test-suite] Move tests requiring FSets
proux01
committed
c62fa4d
[test-suite] Move test requiring FunExt
proux01
committed
ef1ab38
[test-suite] Move test requiring FunInd
proux01
committed
509b853
[test-suite] Move test requiring JMeq
proux01
committed
16e5033
[test-suite] Move tests requiring Lia
proux01
committed
67cd2d4
[test-suite] Move tests requiring List
proux01
committed
2d64b92
[test-suite] Move tests requiring Logic.Eqnotations
proux01
committed
4b5afae
[test-suite] Move test requiring Lra
proux01
committed
ace74e9
[test-suite] Move tests requiring micromega
proux01
committed
4b5a08e
[test-suite] Move tests requiring MSet
proux01
committed
ef4baff
[test-suite] Move tests requiring NArith
proux01
committed
bd8bc6b
[test-suite] Move tests requiring Nsatz
proux01
committed
8615680
[test-suite] Move tests requiring OrderEx
proux01
committed
58a3867
[test-suite] Move test requiring PArith
proux01
committed
7c57fbc
[test-suite] Move test requiring PeanoNat
proux01
committed
c7d8431
[test-suite] Move tests requiring Program
proux01
committed
79913f2
[test-suite] Move tests requiring Program.Equality
proux01
committed
b81f4a7
[test-suite] Move tests requiring Psatz
proux01
committed
e1f8300
[test-suite] Move tests requiring QArith
proux01
committed
ba07932
[test-suite] Move tests requiring Reals
proux01
committed
8d4dafa
[test-suite] Move tests requiring ring
proux01
committed
28f229c
[test-suite] Move tests requiring SetoidClass
proux01
committed
e0bda5f
[test-suite] Move tests requiring SetoidList
proux01
committed
17b5f10
[test-suite] Move tests requiring Sint63
proux01
committed
c2734e7
[test-suite] Move tests requiring String
proux01
committed
87027e2
[test-suite] Move tests requiring Utf8
proux01
committed
190151a
[test-suite] Move tests requiring Vector
proux01
committed
9f1e5cf
[test-suite] Move test requiring Wf_nat
proux01
committed
1b2a6c4
[test-suite] Move tests requiring ZArith
proux01
committed
93d3de9
Move stdlib
proux01
committed
5cece77
[test-suite] Fix misc test after removing stdlib
proux01
committed
5284be7
[stdlib] Adapt README.md and INSTALL.md
proux01
committed
4c1dd87
[stdlib] Add a basic Makefile to compile everything
proux01
committed
06efb58
[stdlib] Adapt Compat
proux01
committed
51423ca
[stdlib] Adapt test-suite
proux01
committed
3c13f60
[stdlib] Compile refman
proux01
committed
6094583
[stdlib] Compile html doc
proux01
committed
7bf21ed
[refman] Add an 'extra' option to '.. coqtop::'
proux01
committed
90ed5be
[refman] Compile the refman mostly without stdlib
proux01
committed
f0c5229
Compile prelude doc without stdlib
proux01
committed
36c9950
Update CONTRIBUTING.md
proux01
committed
1932eaf
Rename OPAM package coq-stdlib -> rocq-core
proux01
committed
5c34b6c
Use Corelib instead of Stdlib as namespace for rocq-core
proux01
committed
4fa4864
Rename target stdlib-html -> corelib-html
proux01
committed
a58bbea
[CI] Add stdlib
proux01
committed
9519a60
[CI] Add refman with all extras
proux01
committed
c3dda1f
Add changelog
proux01
committed
fff68a5
Add overlays
proux01
committed
2dcc49d