Algorithm for populating Trocq database for inductives - #73

Merged

CohenCyril merged 42 commits into

rocq-community:masterfrom

Jun 30, 2026

Commits on Jun 24, 2026

inhab + examples for irrelevance
Tvallejos
committed
c41654b
generating maps with relation10 instead of function
Tvallejos
committed
d61ecb7
generating type of mR | modifications in mymap to get map definition given an inductive
Tvallejos
committed
49b9ed6
common + change of interface + preparing Rm
Tvallejos
committed
01643db
init Rm
Tvallejos
committed
9a0d2dc
structuring
Tvallejos
committed
b86f989
details on injijK
Tvallejos
committed
dcc7b2f
type of mRRmK
Tvallejos
committed
9f02a9f
changing structure
Tvallejos
committed
db3bd6b
collecting injKs
Tvallejos
committed
3ed6bcc
rollback on derivation dep declaration structure
Tvallejos
committed
5044d3c
map4 + umap derivation
Tvallejos
committed
e3dfed6
generating Param40.Rel
Tvallejos
committed
4f49f7d
detailed example derivation for indexed inductives + detailed assembling symK to get paramnn.Rel s
Tvallejos
committed
fc9a452
automatic generation of rel44
Tvallejos
committed
021a60c
wip refactor up-to mymap, build fails for mR
Tvallejos
committed
a835749
generalizing umap program so it generates mapsN instead of just Map4
Tvallejos
committed
2830315
replacing supported generic files + their use in examples/std
Tvallejos
committed
7cacaf6
a hott generalizaion
Tvallejos
committed
d5bac20
a proof of RmmRK
Tvallejos
committed
612c216
wip move theories to generic/inductives + mv elpi to /elpi
Tvallejos
committed
fd82c5e
update in structure
Tvallejos
committed
03e7e4d
improving imports
Tvallejos
committed
870d3c6
removing elpi.lib dependencies
Tvallejos
committed
4245361
fix issue with name overlap in coverage
Tvallejos
committed
39a7e64
generalize inductive generation to universe polymorphism
Tvallejos
committed
3b77308
recovers examples
Tvallejos
committed
89809de
updates dependencies
Tvallejos
committed
9eff89a
removing elpi warnings
Tvallejos
committed
9ad9f4c
coq.typecheck ok
Tvallejos
committed
7d98505
rm comments
Tvallejos
committed
06b97ef
pi + decl into pi-decl + tail-cut
Tvallejos
committed
e7b6084
cleaning outdated files + moving definition of RmmRK
Tvallejos
committed
1705dd6
tidying generalization thm 7.2.2
Tvallejos
committed
87c5d26
accumulating db headers, then files, then dbs
Tvallejos
committed
7275ff5
elpi's accumulate system
Tvallejos
committed
4534d4b
add rocq-elpi to nix
Tvallejos
committed
61e4672
rm mathcomp ssreflect build inputs nix
Tvallejos
committed
64d6e90
update actions
Tvallejos
committed
6fde77a

Commits on Jun 25, 2026

rm outdated db
Tvallejos
committed
339409a
rm superglobal when possible
Tvallejos
committed
26961c2

Commits on Jun 26, 2026

rm synterp hooks require
Tvallejos
committed
e04a747