Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clarify structure #2

Open
wants to merge 181 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
181 commits
Select commit Hold shift + click to select a range
4bfa772
Warn when missing "From Stdlib" in Require
proux01 Jul 20, 2024
4a416fb
Add Bool.Sumbool to prelude
proux01 Dec 17, 2023
8bc1a73
Add reflect to Init
proux01 Dec 17, 2023
193840a
Remove dependency of ssr on Bool
proux01 Jul 4, 2024
b39ef29
Remove dependencies on Extraction and FunExt
proux01 Jul 12, 2024
e3d15da
Restrict dependencies of axioms specifying primitive operators
proux01 Jul 20, 2024
2ce0977
[test-suite] Split tests requiring Arith
proux01 Jul 6, 2024
93735d1
[test-suite] Split tests requiring ZArith
proux01 Jul 5, 2024
9ca9418
[test-suite] Split tests requiring String
proux01 Jul 5, 2024
e125ee2
[test-suite] Split test requiring Lia
proux01 Jul 5, 2024
e11a43c
[test-suite] Cleanup some stdlib dependencies
proux01 Dec 21, 2023
ea38df5
[test-suite] Cleanup dependency on stdlib in ssr
proux01 Jul 4, 2024
22091d8
[test-suite] Cleanup dependencies in primitive/arrays
proux01 Jul 4, 2024
8648dbe
[test-suite] Cleanup dependencies in primitive/float
proux01 Jul 4, 2024
5a8e17a
[test-suite] Cleanup dependencies in primitive/string
proux01 Jul 5, 2024
ad1e1bc
[test-suite] Cleanup dependencies in primitive/int63
proux01 Jul 5, 2024
1c29f94
[test-suite] Cleanup dependencies on Arith
proux01 Jul 5, 2024
81f3771
[test-suite] Cleanup dependency on Extraction
proux01 Jul 15, 2024
6189fba
[test-suite] Cleanup dependency in Floats
proux01 Jul 5, 2024
a74847e
[test-suite] Cleanup dependencies on List
proux01 Jul 15, 2024
a72d3f2
[test-suite] Cleanup dependencies on NArith
proux01 Jul 15, 2024
5b1f0f6
[test-suite] Cleanup dependency on PArray
proux01 Jul 5, 2024
c4c96d0
[test-suite] Cleanup dependencies on PArith
proux01 Jul 5, 2024
3edd85e
[test-suite] Cleanup dependencies on Program
proux01 Jul 5, 2024
523f76d
[test-suite] Cleanup dependency on RelationClasses
proux01 Jul 5, 2024
40faafb
[test-suite] Cleanup dependency on Relations
proux01 Jul 5, 2024
6d0647b
[test-suite] Cleanup dependencies on String
proux01 Jul 15, 2024
77b7cb0
[test-suite] Cleanup dependencies on Uint63
proux01 Jul 5, 2024
3ff4352
[test-suite] Cleanup dependencies on Utf8
proux01 Jul 5, 2024
9d1e7b4
[test-suite] Cleanup dependencies on ZArith
proux01 Jul 15, 2024
c743f35
[test-suite] Cleanup dependeny on Bool
proux01 Jul 14, 2024
5d366aa
[test-suite] Cleanup dependency on FunExt
proux01 Jul 15, 2024
6775684
[test-suite] Cleanup dependencies on FunInd
proux01 Jul 14, 2024
bc92487
[test-suite] Cleanup dependencies on Hurkens
proux01 Jul 14, 2024
fe09292
[test-suite] Cleanup dependency on JMeq
proux01 Jul 14, 2024
f104bd6
[test-suite] Move tests requiring Arith
proux01 Oct 12, 2024
0ee05f8
[test-suite] Move test requiring Bool
proux01 Oct 12, 2024
95ad293
[test-suite] Move tests requiring btauto
proux01 Oct 12, 2024
13f1f26
[test-suite] Move test requiring CEquivalence
proux01 Oct 12, 2024
3cd364b
[test-suite] Move test requiring Classes.Equivalence
proux01 Oct 12, 2024
9a1b05c
[test-suite] Move test requiring Classical
proux01 Oct 12, 2024
e1b482e
[test-suite] Move test requiring Classical_prop
proux01 Oct 12, 2024
3b09203
[test-suite] Move test requiring Cyclic
proux01 Oct 12, 2024
578e30c
[test-suite] Move test requiring DecidableClasses
proux01 Oct 12, 2024
6cbc0cd
[test-suite] Move tests requiring Ensembles
proux01 Oct 12, 2024
357a331
[test-suite] Move tests requiring Eqdep
proux01 Oct 12, 2024
912aea1
[test-suite] Move tests requiring Equality
proux01 Oct 12, 2024
2de51c3
[test-suite] Move tests requiring EquivDec
proux01 Oct 12, 2024
b613db7
[test-suite] Move test requiring field
proux01 Oct 12, 2024
ee17daa
[test-suite] Move test requiring Floats
proux01 Oct 12, 2024
51115c1
[test-suite] Move tests requiring FSets
proux01 Oct 12, 2024
7f99d33
[test-suite] Move test requiring FunExt
proux01 Oct 12, 2024
79fa153
[test-suite] Move test requiring FunInd
proux01 Oct 12, 2024
6a9b3de
[test-suite] Move test requiring JMeq
proux01 Oct 12, 2024
0d0cc60
[test-suite] Move tests requiring Lia
proux01 Oct 12, 2024
7aed9ce
[test-suite] Move tests requiring List
proux01 Oct 12, 2024
bb7c9f4
[test-suite] Move tests requiring Logic.Eqnotations
proux01 Oct 12, 2024
803045d
[test-suite] Move test requiring Lra
proux01 Oct 12, 2024
196e784
[test-suite] Move tests requiring micromega
proux01 Oct 12, 2024
81df4cb
[test-suite] Move tests requiring MSet
proux01 Oct 12, 2024
a60229c
[test-suite] Move tests requiring NArith
proux01 Oct 12, 2024
594dee8
[test-suite] Move tests requiring Nsatz
proux01 Oct 12, 2024
7b7a7b8
[test-suite] Move tests requiring OrderEx
proux01 Oct 12, 2024
37bcd5b
[test-suite] Move test requiring PArith
proux01 Oct 12, 2024
ca79e0c
[test-suite] Move test requiring PeanoNat
proux01 Oct 12, 2024
bde082b
[test-suite] Move tests requiring Program
proux01 Oct 12, 2024
2f66d6f
[test-suite] Move tests requiring Program.Equality
proux01 Oct 12, 2024
3354eb2
[test-suite] Move tests requiring Psatz
proux01 Oct 12, 2024
04261e3
[test-suite] Move tests requiring QArith
proux01 Oct 12, 2024
ead88b4
[test-suite] Move tests requiring Reals
proux01 Oct 12, 2024
d08cb13
[test-suite] Move tests requiring ring
proux01 Oct 12, 2024
78425ee
[test-suite] Move tests requiring SetoidClass
proux01 Oct 12, 2024
b0f80b0
[test-suite] Move tests requiring SetoidList
proux01 Oct 12, 2024
a71c19b
[test-suite] Move tests requiring Sint63
proux01 Oct 12, 2024
ae3a4af
[test-suite] Move tests requiring String
proux01 Oct 12, 2024
f2439ea
[test-suite] Move tests requiring Utf8
proux01 Oct 12, 2024
de271cd
[test-suite] Move tests requiring Vector
proux01 Oct 12, 2024
ea086f5
[test-suite] Move test requiring Wf_nat
proux01 Oct 12, 2024
f23f27c
[test-suite] Move tests requiring ZArith
proux01 Oct 12, 2024
c3d483a
Move stdlib
proux01 Oct 12, 2024
8004347
[test-suite] Fix misc test after removing stdlib
proux01 Sep 18, 2024
ae167a5
[stdlib] Adapt README.md and INSTALL.md
proux01 Jul 30, 2024
9fbc2f2
[stdlib] Add a basic Makefile to compile everything
proux01 Sep 26, 2024
718f377
[stdlib] Adapt Compat
proux01 Oct 12, 2024
abd2209
[stdlib] Adapt test-suite
proux01 Jul 10, 2024
a475676
[stdlib] Compile refman
proux01 Oct 12, 2024
9d4da58
[stdlib] Compile html doc
proux01 Oct 12, 2024
2a7c4dd
[refman] Add an 'extra' option to '.. coqtop::'
proux01 Oct 23, 2024
1be72b5
[refman] Compile the refman mostly without stdlib
proux01 Oct 8, 2024
804276c
Compile prelude doc without stdlib
proux01 Jul 11, 2024
a8d0ed4
Update CONTRIBUTING.md
proux01 Jul 29, 2024
7d910a7
Rename OPAM package coq-stdlib -> rocq-init
proux01 Aug 1, 2024
19efd8e
[CI] Add stdlib
proux01 Sep 12, 2024
388389b
[CI] Add refman with all extras
proux01 Oct 23, 2024
de2f1be
Add overlays
proux01 Sep 12, 2024
37883e1
Add changelog
proux01 Sep 15, 2024
a187b32
Keep a few files in stdlib
proux01 Oct 15, 2024
f2a701d
Remove all but stdlib
proux01 Oct 15, 2024
3805e70
Move stdlib
proux01 Oct 15, 2024
5f43cea
Adapt changelog
proux01 Oct 16, 2024
4e4f33a
Adapt CONTRIBUTING.md
proux01 Oct 15, 2024
5905e92
Update Pull Request template
proux01 Aug 1, 2024
1143e06
Adapt CI
proux01 Sep 21, 2024
472b1cd
[CI] Add a job to run test-suite
proux01 Aug 2, 2024
c21e702
[CI] Add a job refman-html
proux01 Aug 4, 2024
e41231a
[CI] Add a job stdlib-html
proux01 Aug 4, 2024
f67bccd
[CI] Retrieve lint job
proux01 Aug 2, 2024
7996192
[CI] Add a README
proux01 Aug 1, 2024
3d7797b
Change -R to -Q
proux01 Dec 17, 2023
1937a98
Compile ConstructiveEpsilon without Arith
proux01 Dec 14, 2023
fb0e7e8
Compile WeakFan without List
proux01 Dec 14, 2023
aa83e9c
Compile RelationPairs without SetoidList
proux01 Dec 14, 2023
2572ef6
Compile Classes.SetoidDec without Arith
proux01 Dec 16, 2023
0548c93
Compile Cantor.v without micromega
proux01 Dec 15, 2023
313b1c1
Compile Logic/WKL without Arith
proux01 Dec 16, 2023
347a72e
Compile NArith without ring
proux01 Dec 15, 2023
d0efd3b
Compile ZArith without QArith
proux01 Dec 16, 2023
b2b4ade
Compile NsatzTactic without QArith
proux01 Jul 12, 2024
6baf90f
Compile Floats without Psatz
proux01 Dec 16, 2023
3e32e1c
Compile lists without positive
proux01 Jul 7, 2024
900530e
Move FinFun and Bvector to Vectors
proux01 Jul 7, 2024
2149b44
Move Qreals from QArith to Reals
proux01 Jul 7, 2024
9f8fff8
Move SetoidList and SetoidPermutation from Lists to Sorting
proux01 Jul 7, 2024
af41e27
Move BoolOrder from Bool to Structures
proux01 Jul 7, 2024
c60abbd
Move Zerob from Bool to Arith
proux01 Jul 7, 2024
99730b3
Move Nsatz from nsatz to Reals
proux01 Jul 12, 2024
ab77ab4
Move Streams to their own directory
proux01 Sep 26, 2024
16ea617
Move MExtraction from micromega to test-suite
proux01 Jul 15, 2024
3ebbf05
Detail _CoqProject
proux01 Sep 26, 2024
dfbc314
Split Logic into subdirectories Base, Classical and Lists
proux01 Jul 7, 2024
a13f5d9
Split Classes into subdirectories All, Arith and Lists
proux01 Sep 26, 2024
101be70
Split Numbers into subdirectories Arith, List, positive, Z, Q, R and …
proux01 Jul 7, 2024
33ca66c
Split Structures into subdirectories Def and Ex
proux01 Jul 7, 2024
bda196b
Split Arith into subdirectories All and Base
proux01 Jul 7, 2024
dd31bb8
Split ZArith into subdirectories All, Base and Ring
proux01 Jul 7, 2024
c73719b
Split QArith into subdirectories All, Base and Field
proux01 Jul 7, 2024
3529e60
Split setoid_ring into subdirectories Q, R and Z
proux01 Jul 7, 2024
566c65f
Split micromega into subdirectories Int63, Lia, Lqa, Lra and Zify
proux01 Jul 7, 2024
bfc8e8b
Add dependency graph
proux01 Jul 11, 2024
7c62bbd
Add Makefile for logic
proux01 Sep 28, 2024
f0fe484
Add Makefile for streams
proux01 Jul 12, 2024
bd3f761
Add Makefile for program
proux01 Dec 17, 2023
d278bec
Add Makefile for Relations
proux01 Dec 17, 2023
5dd074e
Add Makefile for classes
proux01 Dec 17, 2023
d876d38
Add Makefile for bool
proux01 Dec 17, 2023
cf4573b
Add Makefile for structures
proux01 Dec 17, 2023
f53cbc6
Add Makefile for arith-base
proux01 Dec 17, 2023
c50168a
Add Makefile for list
proux01 Dec 17, 2023
8bb83c1
Add Makefile for positive
proux01 Dec 17, 2023
de589c4
Add Makefile for narith
proux01 Jul 7, 2024
6025d3d
Add Makefile for zarith-base
proux01 Jul 7, 2024
1f134a5
Add Makefile for ring
proux01 Jul 7, 2024
1e9ff84
Add Makefile for arith
proux01 Jul 7, 2024
0ad504e
Add Makefile for lia
proux01 Jul 7, 2024
220b355
Add Makefile for zarith
proux01 Jul 7, 2024
3127926
Add Makefile for unicode
proux01 Dec 17, 2023
32bd2ec
Add Makefile for primitive-int
proux01 Jul 7, 2024
598d49e
Add Makefile for primitive-array
proux01 Jul 7, 2024
18e1d06
Add Makefile for vectors
proux01 Jul 7, 2024
1a4b542
Add Makefile for string
proux01 Jul 7, 2024
ffc24db
Add Makefile for classical-logic
proux01 Jul 7, 2024
50ee031
Add Makefile for sets
proux01 Jul 7, 2024
776d671
Add Makefile for sorting
proux01 Jul 7, 2024
9b351d8
Add Makefile for orders-ex
proux01 Jul 7, 2024
f2458a2
Add Makefile for primitive-string
proux01 Jul 7, 2024
f195fff
Add Makefile for primitive-floats
proux01 Jul 7, 2024
2dfd138
Add Makefile for extraction
proux01 Dec 17, 2023
a0a475a
Add Makefile for funind
proux01 Dec 17, 2023
a61e48c
Add Makefile for qarith-base
proux01 Jul 8, 2024
d550745
Add Makefile for field
proux01 Jul 8, 2024
42088ff
Add Makefile for lqa
proux01 Jul 8, 2024
cb5ad72
Add Makefile for qarith
proux01 Jul 8, 2024
cc9f571
Add Makefile for nsatz
proux01 Dec 17, 2023
8de036d
Add Makefile for reals
proux01 Dec 17, 2023
996b465
Add Makefile for fmaps-fsets-msets
proux01 Jul 12, 2024
5d14867
Add Makefile for wellfounded
proux01 Dec 17, 2023
856b92e
Add Makefile for rtauto
proux01 Dec 17, 2023
b915bfe
Add Makefile for compat
proux01 Sep 28, 2024
91fe0f1
[CI] Add a job to check the subcomponent structure
proux01 Jul 30, 2024
47c9ec5
[CI] Add a job to check makefiles
proux01 Jul 30, 2024
e37e2ff
[CI] Add a job to check for duplicate files
proux01 Jul 30, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
[test-suite] Cleanup dependency on RelationClasses
proux01 committed Oct 24, 2024
commit 523f76d71116a3aa05d4eb3921afe0a70e9d8ff3
1 change: 1 addition & 0 deletions test-suite/bugs/bug_4503.v
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
Require RelationClasses.
Require TestSuite.relationclasses.

Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=