Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
946 commits
Select commit Hold shift + click to select a range
07604ff
Merge PR #21953: Compute rocqdep dependencies on demand.
coqbot-app[bot] Apr 25, 2026
bc4c329
Optimize the algorithm for unicode validation.
ppedrot Apr 24, 2026
6707510
Merge PR #21885: Validate Proof: detect missing constraints, error if…
coqbot-app[bot] Apr 26, 2026
a47999d
Merge PR #21961: Optimize the algorithm for unicode validation.
coqbot-app[bot] Apr 27, 2026
8998902
dune test_suite_config.inc rule use rocq instead of coqc
SkySkimmer Apr 24, 2026
b378d82
Fix ci-refman artifact handling
SkySkimmer Apr 27, 2026
ed0115c
Avoid conflict between global sorts defined in separate modules
SkySkimmer Apr 24, 2026
673fe17
Merge PR #21959: dune test_suite_config.inc rule use rocq instead of …
coqbot-app[bot] Apr 27, 2026
e7cf080
push_subgraph avoid looking at irrelevant parts of the graph
SkySkimmer Apr 11, 2026
7a06dbb
Some Makefile targets integrate with make jobserver
SkySkimmer Apr 21, 2026
3a26bca
Add note to Ltac2 docs for sequence and dispatching
Durbatuluk1701 Apr 26, 2026
84f874a
Minor cleanup in rocqdep internal data structures.
ppedrot Apr 26, 2026
1ba814e
Purify the internals of Loadpath.add_directory.
ppedrot Apr 27, 2026
64ea87c
Clean up internals of rocqdep around warn_if_clash.
ppedrot Apr 27, 2026
0b934b6
ci: use Elpi 3.7.0
gares Apr 16, 2026
ac62268
Merge PR #21915: push_subgraph avoid looking at irrelevant parts of t…
coqbot-app[bot] Apr 28, 2026
456b815
Merge PR #21963: Fix ci-refman artifact handling
coqbot-app[bot] Apr 28, 2026
f43cf8f
Fix ci-refman artifact handling (for real this time?)
SkySkimmer Apr 28, 2026
c6d8b0f
Merge PR #21965: Minor cleanup of rocqdep internals
coqbot-app[bot] Apr 28, 2026
f1e8be7
Merge PR #21962: Add note to Ltac2 docs for sequence and dispatching
coqbot-app[bot] Apr 28, 2026
4853c47
Merge PR #21967: Fix ci-refman artifact handling (for real this time?)
coqbot-app[bot] Apr 28, 2026
c6d2a48
Warning for missing "Proof" command and error on duplicate or late "P…
SkySkimmer Apr 1, 2026
58360cb
Add coqargs to dune-dbg -I
SkySkimmer Apr 29, 2026
dfb9aa7
Remove double universe substitution in branches
yannl35133 Apr 28, 2026
d737b5e
Use Unix file descriptors rather than OCaml channels in rocqdep.
ppedrot Apr 23, 2026
4185712
Faster skip_to_dot in rocqdep lexer.
ppedrot Apr 25, 2026
77fcac6
Small optimization in rocqdep.
ppedrot Apr 26, 2026
8981506
Do not create intermediate lists in rocqdep directory traversal.
ppedrot Apr 27, 2026
8282a0c
Do not create intermediate strings in rocqdep makefile printing.
ppedrot Apr 27, 2026
71202f2
Merge PR #21957: Avoid conflict between global sorts defined in separ…
coqbot-app[bot] Apr 29, 2026
8ef6beb
Merge PR #21969: Optimize various hotspots in rocqdep
coqbot-app[bot] Apr 29, 2026
606731b
Merge PR #21972: Remove double universe substitution in branches
coqbot-app[bot] Apr 29, 2026
88aa5b0
Move number notation declarations to their respective modules instead…
SkySkimmer Apr 28, 2026
14741e1
Merge PR #21924: ci: use Elpi 3.7.1
coqbot-app[bot] Apr 29, 2026
a1206a1
Abstract away the definition the opacity-tracking structure in rocqchk.
ppedrot Apr 29, 2026
9e9a921
Clean up function CClosure.get_branch
yannl35133 Apr 28, 2026
b4943df
Merge PR #21974: Add coqargs to dune-dbg -I
coqbot-app[bot] Apr 29, 2026
875b943
Add `Hint Mode =` to freeze corresponding evars in TC queries
Janno Apr 10, 2026
90e518d
Update grammar
Janno Apr 30, 2026
0fad295
Update documentation
Janno Apr 30, 2026
b050918
Merge PR #21865: Warning for missing "Proof" command and error on dup…
coqbot-app[bot] Apr 30, 2026
cfca8cd
Use Id.equal instead of Id.compare = 0 in push_rel_decl_to_named_context
SkySkimmer Apr 30, 2026
bab23ad
Merge PR #21978: Abstract away the definition the opacity-tracking st…
coqbot-app[bot] Apr 30, 2026
c441de8
Remove Context.Compacted.Declaration.to_named_context
SkySkimmer Apr 30, 2026
c39e67d
Remove unused Termops.push_named_rec_types
SkySkimmer Apr 30, 2026
e628fff
Remove unused argument in checker internals.
ppedrot Apr 30, 2026
c736c8b
Static invariant that rocqchk opaque data only contains pure kernames.
ppedrot Apr 29, 2026
d441c0b
Factorize the internals of opaque computation in rocqchk.
ppedrot Apr 29, 2026
ae5bffb
Rely on user-facing names for rocqchk opaque analysis.
ppedrot Apr 30, 2026
7d4ee21
Merge PR #21980: Use Id.equal instead of Id.compare = 0 in push_rel_d…
coqbot-app[bot] Apr 30, 2026
c36b0c9
Merge PR #21560: setoid rewriting: improve support for forall_relation
coqbot-app[bot] Apr 30, 2026
5da098a
Stop relying on canonical equality in Inductiveops.
ppedrot Apr 30, 2026
b7e9b22
Merge PR #21911: Add `Hint Mode =` to freeze corresponding evars in T…
coqbot-app[bot] Apr 30, 2026
6b773fd
Merge PR #21983: Remove unused Termops.push_named_rec_types
coqbot-app[bot] Apr 30, 2026
4966e92
Merge PR #21971: Move number notation declarations to their respectiv…
coqbot-app[bot] Apr 30, 2026
ba7ed56
Stop relying on canonizing GlobRef.Map in hint internals.
ppedrot Apr 30, 2026
1f0b83b
Add overlays.
ppedrot May 1, 2026
2f4c858
Merge PR #21973: Clean up function CClosure.get_branch
coqbot-app[bot] May 1, 2026
b5d0109
rocqide -xml-debug does not imply -debug
SkySkimmer May 1, 2026
9268c79
rocqide get background goals when needed
SkySkimmer May 1, 2026
2f5b7a2
Inline some constant arguments in rocqide
SkySkimmer May 1, 2026
f8ec577
Merge PR #21991: Inline some constant arguments in rocqide
coqbot-app[bot] May 3, 2026
46e8103
Merge PR #21988: rocqide -xml-debug does not imply -debug
coqbot-app[bot] May 3, 2026
f6f6116
Merge PR #21990: rocqide get background goals when needed
coqbot-app[bot] May 3, 2026
394d025
Ltac2 share some code between lazy_match and multi_match
SkySkimmer May 3, 2026
7f472df
Merge PR #21985: Stop relying on canonical equality in Inductiveops.
coqbot-app[bot] May 3, 2026
9bef87f
Merge PR #21981: Rely on user-facing names for rocqchk opaque analysis.
coqbot-app[bot] May 3, 2026
df88c3c
Merge PR #21986: Stop relying on canonizing GlobRef.Map in hint inter…
coqbot-app[bot] May 3, 2026
644c907
Stop relying on GlobRef.Map in Zify internals.
ppedrot May 3, 2026
660eaad
Deprecate the GlobRef.Map module.
ppedrot May 3, 2026
72979f4
Minor code factorization in Declareops.
ppedrot May 4, 2026
116142d
`Strict Resolution` has precedence over `Hint Mode`
Janno May 4, 2026
0a16eef
Merge PR #21994: Minor code factorization in Declareops.
coqbot-app[bot] May 4, 2026
a8acbe4
Print external hints before running them
Janno Apr 7, 2026
2cb9b48
Merge PR #21993: Deprecate the GlobRef.Map module.
coqbot-app[bot] May 4, 2026
7f41334
Merge PR #21950: Create `rocq doc` backend for Alectryon
coqbot-app[bot] May 4, 2026
e1c522a
Inline canonical equality in kernel subtyping.
ppedrot May 4, 2026
fc4dbca
Merge PR #21982: Remove Context.Compacted.Declaration.to_named_context
coqbot-app[bot] May 4, 2026
266d71e
Simpler implementation of undefined_evars_cache
SkySkimmer Apr 30, 2026
75a3e91
Introduce user-based sets and maps for projections.
ppedrot May 4, 2026
4359cc8
Expose userord-based sets for unfoldable globals in hint databases.
ppedrot May 4, 2026
a4996be
Remove non needed check_required_library in Generalize.abstract_args
SkySkimmer May 4, 2026
adc572a
Rely on user name equality for kernel conversion fast path.
ppedrot May 4, 2026
f71b893
Add overlays.
ppedrot May 5, 2026
3717a11
Merge PR #21899: TC search: log hint before hint is applied
coqbot-app[bot] May 5, 2026
33609b8
Correctly expand included modules in Declaremods "with Module".
ppedrot May 5, 2026
5c13916
generalize_eqs_vars fix incorrect selection of variables to generalize
SkySkimmer May 4, 2026
7aa7dd1
Don't use Qed to avoid async proofs in TC debug output test
SkySkimmer May 5, 2026
eca06c0
Merge PR #17266: Command modifier and tactic for allocation limits
coqbot-app[bot] May 5, 2026
2e3001b
Merge PR #21998: Inline canonical equality in kernel subtyping.
coqbot-app[bot] May 5, 2026
91be8a4
Merge PR #21999: Expose userord-based sets for unfoldable globals in …
coqbot-app[bot] May 5, 2026
857ec00
Merge PR #22002: Rely on user name equality for kernel conversion fas…
coqbot-app[bot] May 5, 2026
20c0f2b
Merge PR #22003: Correctly expand included modules in Declaremods "wi…
coqbot-app[bot] May 5, 2026
24ae978
Profiler attempt to measure heap size
SkySkimmer Apr 23, 2026
f27a42e
timelog2html visuals for heap usage
SkySkimmer Apr 24, 2026
b77272f
Make RR variables not being unifiable structural
yannl35133 May 5, 2026
1f1d459
Prevent downcast on RR evars
yannl35133 Apr 14, 2026
d1f11db
Undo adhoc exclusion of RR evar unification
yannl35133 May 5, 2026
595aee7
Deprecate the canord-based PRset and PRmap modules from the Names API.
ppedrot May 6, 2026
90f1837
Do not perform useless context type conversions in Logic reordering.
ppedrot May 6, 2026
f74e111
Merge PR #22005: Don't use Qed to avoid async proofs in TC debug outp…
coqbot-app[bot] May 6, 2026
e778a64
Merge PR #21992: Ltac2 share some code between lazy_match and multi_m…
coqbot-app[bot] May 6, 2026
0a94db5
Merge PR #21948: Profiler attempt to measure change in heap size
coqbot-app[bot] May 6, 2026
4829038
Merge PR #21940: Some Makefile targets integrate with make jobserver
coqbot-app[bot] May 6, 2026
f2654bb
Merge PR #22006: Deprecate the canord-based PRset and PRmap modules f…
coqbot-app[bot] May 6, 2026
af3cabc
Merge PR #22007: Do not perform useless context type conversions in L…
coqbot-app[bot] May 6, 2026
f2f00a4
Use quotiented constant maps in Dumpglob.
ppedrot May 6, 2026
9ca46cb
Use quotiented constant maps in Reductionops.
ppedrot May 6, 2026
4760802
Deprecate the canord-based maps and sets of constants.
ppedrot May 6, 2026
0a4fc5d
Merge PR #22008: Deprecate the canord-based maps and sets of constants.
coqbot-app[bot] May 7, 2026
32f2cb2
Fix nametab handling when printing abbreviation
SkySkimmer May 7, 2026
9d8ff35
Bench automatic overlay system
SkySkimmer May 7, 2026
c83f03b
Update default package list in bench after rocq-prover/opam#3726
SkySkimmer May 10, 2026
4a3c795
Merge PR #22015: Update default package list in bench after rocq-prov…
coqbot-app[bot] May 11, 2026
f69fce1
Allow setting a root in AcyclicGraph.
ppedrot Mar 28, 2026
39cbebe
Keep track of components in AcyclicGraph data structure.
ppedrot Mar 28, 2026
bfc706e
Remove root from AcyclicGraph internal graph.
ppedrot Mar 30, 2026
90f587b
Constr-as-datatype functions now use the user name for references.
ppedrot Apr 3, 2026
8a4aa7d
Reduce the exposure of QualityOrSet.t type in the Retyping API.
ppedrot May 12, 2026
491239d
Add overlays.
ppedrot May 12, 2026
321ff69
Have {find,drop}_uniform_parameters work with mutual fixpoints correctly
yannl35133 May 12, 2026
42f8ebc
Always check nested fix lambda domains
yannl35133 May 13, 2026
a81c284
add test
yannl35133 May 13, 2026
d53a458
Generalize About to allow printing several definitions
thomas-lamiaux May 8, 2026
2dab698
Simplification of elim unification flags.
ppedrot May 16, 2026
a4da4e6
Merge PR #21997: `Strict Resolution` has precedence over `Hint Mode`
coqbot-app[bot] May 18, 2026
d3a9eea
coqloop move resynch_buffer inside read_eand_execute try block
SkySkimmer May 18, 2026
5ee2850
Remove duplicate package check in bench
SkySkimmer May 18, 2026
c304415
Merge PR #22011: Bench automatic overlay system
coqbot-app[bot] May 18, 2026
0d4ec29
Merge PR #21823: Generalize About to Print Several Definitions
coqbot-app[bot] May 18, 2026
518bc51
Merge PR #22014: Special handling of root node in AcyclicGraph algorithm
coqbot-app[bot] May 18, 2026
138fbe9
Merge PR #22016: Reduce the exposure of QualityOrSet.t type in the Re…
coqbot-app[bot] May 18, 2026
ae510f4
Merge PR #21882: Constr-as-datatype functions now use the user name f…
coqbot-app[bot] May 18, 2026
10e5579
Merge PR #22031: Remove duplicate package check in bench
coqbot-app[bot] May 18, 2026
7311bac
Add critical bug entry
yannl35133 May 18, 2026
05b9320
Merge PR #22030: coqloop move resynch_buffer inside read_eand_execute…
coqbot-app[bot] May 18, 2026
0aeb0e0
Generalize Print to print multiple arguments
FloraStorm May 12, 2026
1139756
Propagate a constant argument in Rewrite internal.
ppedrot May 19, 2026
d1dd107
Decouple the Hints.hint_ast type from the API from its internal version.
ppedrot Apr 4, 2026
fcf3679
Inline the now static parameter in user-facing Hints.hint_ast.
ppedrot Apr 4, 2026
1a59d2f
Merge PR #22017: Generalize Print to print multiple arguments
coqbot-app[bot] May 19, 2026
c3e0e67
Merge PR #22001: generalize_eqs_vars fix incorrect selection of vari…
coqbot-app[bot] May 19, 2026
8ed93d6
Add tests
yannl35133 May 19, 2026
a356363
Remove the unused AcyclicGraph.choose primitive.
ppedrot May 19, 2026
f1b2faa
Merge PR #22022: Always check nested fix lambda domains
coqbot-app[bot] May 19, 2026
50e0f1a
Merge PR #21984: Simpler implementation of undefined_evars_cache
coqbot-app[bot] May 19, 2026
edb1057
Merge PR #22010: Fix nametab handling when printing abbreviation
coqbot-app[bot] May 19, 2026
20832b1
Merge PR #22039: Remove the unused AcyclicGraph.choose primitive.
coqbot-app[bot] May 19, 2026
6ad57e1
Merge PR #22038: Internal tweaks to the Hints API
coqbot-app[bot] May 19, 2026
61708f7
Merge PR #22034: Propagate a constant argument in Rewrite internal.
coqbot-app[bot] May 19, 2026
4df9cb0
Merge PR #21936: rocqmakefile avoid using make's filter on full sourc…
coqbot-app[bot] May 20, 2026
0f85cf5
Laxer normal form criterion for strong kernel normalization.
ppedrot May 18, 2026
bc07551
Merge PR #22032: Laxer normal form criterion for strong kernel normal…
coqbot-app[bot] May 20, 2026
f018a77
Merge PR #21912: Make RR variables not being unifiable a default flag
coqbot-app[bot] May 20, 2026
623c073
Faster type-based fast path in Unification.w_unify_to_subterm_all.
ppedrot May 19, 2026
f1678ff
Merge PR #22028: Simplification of elim unification flags.
coqbot-app[bot] May 20, 2026
4f5b9b4
Merge PR #22040: Faster type-based fast path in Unification.w_unify_t…
coqbot-app[bot] May 21, 2026
650c605
Merge PR #22018: Have {find,drop}_uniform_parameters work with mutual…
coqbot-app[bot] May 21, 2026
ba47641
Remove compat coq-core libraries (not executables)
SkySkimmer Apr 24, 2026
b192ed8
Test for uniform parameters with correct bounds
yannl35133 May 22, 2026
0d0188b
Don't use Lazy in the parser
SkySkimmer May 22, 2026
f6fb84b
Stop using global lazys in micromega
SkySkimmer May 22, 2026
0160e8c
Stop using global lazy in zify
SkySkimmer May 22, 2026
1ad84d5
Stop using global lazy for temp dir in nativelib
SkySkimmer May 22, 2026
6904ddd
Stop using global lazy in tactics/
SkySkimmer May 22, 2026
b9e64ca
Stop using global lazy in cctac
SkySkimmer May 22, 2026
c030c96
Stop using global lazy in rtauto
SkySkimmer May 22, 2026
9b4c355
Stop using global lazy in funind
SkySkimmer May 22, 2026
186e567
docker: install memprof-limits
gares May 22, 2026
c0b8da9
Merge PR #22056: docker: install memprof-limits
coqbot-app[bot] May 22, 2026
27c28ee
Merge PR #22055: Stop using global lazy in funind
coqbot-app[bot] May 23, 2026
2e25e3a
Merge PR #22054: Stop using global lazy in rtauto
coqbot-app[bot] May 23, 2026
93ab36b
Merge PR #22052: Stop using global lazy in tactics/
coqbot-app[bot] May 23, 2026
a021803
Merge PR #22053: Stop using global lazy in cctac
coqbot-app[bot] May 23, 2026
3006a6d
Fix contract_case anomaly: reimplement with evar-aware decomposition
JasonGross May 24, 2026
e4375c5
Merge PR #22051: Stop using global lazy for temp dir in nativelib
coqbot-app[bot] May 26, 2026
956619d
Merge PR #22061: Fix contract_case anomaly: reimplement with evar-awa…
coqbot-app[bot] May 26, 2026
7f0de77
Merge PR #22047: Test for uniform parameters with correct bounds
coqbot-app[bot] May 26, 2026
3b3c606
Merge PR #22048: Don't use Lazy in the parser
coqbot-app[bot] May 26, 2026
fc4194f
Give primitive eta when elimination checks are disabled
ebmoon May 26, 2026
d230edc
Merge PR #22050: Stop using global lazys in micromega
coqbot-app[bot] May 27, 2026
44fe4b9
[CI] Fix mathcomp
proux01 May 27, 2026
5aa64e5
Merge PR #22071: [CI] Fix mathcomp (add micromega separate repo)
coqbot-app[bot] May 27, 2026
60a62d1
[CI] Fix mathcomp test
proux01 May 28, 2026
505d8f6
[CI] Fix jasmin
proux01 May 28, 2026
22f4a45
[CI] Remove algebra tactics
proux01 May 28, 2026
9805aff
Merge PR #22073: [CI] Fix jasmin and mathcomp-test
coqbot-app[bot] May 28, 2026
980c7ea
Keep track of variable status (secvar or not) in named contexts
SkySkimmer Apr 30, 2026
45e9c60
check_hyps_inclusion use variable status instead of conversion
SkySkimmer Apr 30, 2026
0c35e6b
Error instead of renaming section variable mentioned through a global
SkySkimmer Apr 30, 2026
9eef589
Tactics.clear handle unbound ids
SkySkimmer May 4, 2026
78b65e7
Use variable status to decide if a variable is section variable
SkySkimmer Apr 30, 2026
44ee3d2
changelog for section variable status tracking
SkySkimmer May 19, 2026
d52593d
better error message for ReferenceVariables for secvar status mismatch
SkySkimmer May 19, 2026
4efd00c
slightly streamline pr_context_of code
SkySkimmer May 19, 2026
8d6ddc0
Move CompactedDecl to ppconstr
SkySkimmer May 19, 2026
ff75bf4
Debug flag for variable status
SkySkimmer May 19, 2026
f977070
uncomment assert in environ
SkySkimmer May 20, 2026
3452ac2
bench auto overlays for metarocq
SkySkimmer May 21, 2026
395a8d8
add is_section_var tactic
SkySkimmer May 27, 2026
9fd9307
overlay
SkySkimmer May 20, 2026
db31970
weaken assert in push_named
SkySkimmer May 27, 2026
5315327
Remove more global lazys
SkySkimmer May 28, 2026
9b7f986
Merge PR #21952: Always provide primitive eta when `check_elimination…
coqbot-app[bot] May 28, 2026
01d2f00
Have implicit arguments with "Asymmetric Patterns"
proux01 Apr 14, 2026
0ff5c74
Improve pattern externalization with Asymettric Patterns
proux01 Apr 14, 2026
20d7787
Makefile.ci use wildcard instead of exhaustive list of CI_TARGETS
SkySkimmer May 28, 2026
7447c24
Reduction effects use econstr
SkySkimmer May 28, 2026
eb2d03d
Avoid printing missing-scheme warning when rewrite fails
SkySkimmer May 28, 2026
66dc56d
disable some not needed overlays
SkySkimmer May 28, 2026
606d39a
Merge PR #21955: Remove compat coq-core libraries (not executables)
coqbot-app[bot] May 28, 2026
3353405
[CI] Fix micromega dune package name
proux01 May 29, 2026
cb1f976
Merge PR #22083: [CI] Fix micromega dune package name
coqbot-app[bot] May 29, 2026
8777cc1
Stop explicitly starting memprof limits
SkySkimmer May 29, 2026
1fc7ef0
Merge PR #21947: Have implicit arguments with "Asymmetric Patterns"
coqbot-app[bot] May 29, 2026
343989f
Merge PR #22084: Stop explicitly starting memprof limits
coqbot-app[bot] May 29, 2026
40538c7
Correctly handle iris projects in ci-reset script.
ppedrot May 30, 2026
112b50c
Do not return the inductive entry in IndTyping.get_template.
ppedrot Dec 10, 2025
d3f3786
Preserve bound universe names in template inductive types.
ppedrot Dec 10, 2025
921ad1d
Store template inductive data abstracted w.r.t. template levels.
ppedrot Mar 10, 2026
66be664
Add overlays.
ppedrot May 28, 2026
3ed13a4
Merge PR #22075: Makefile.ci use wildcard instead of exhaustive list …
coqbot-app[bot] Jun 1, 2026
0f1cf6a
Merge PR #22085: Correctly handle iris projects in ci-reset script.
coqbot-app[bot] Jun 1, 2026
60156a0
Rename is_section_variable' -> is_section_variable_env
SkySkimmer Jun 1, 2026
eebacb3
Merge PR #21987: Keep track of which variables are section variables …
coqbot-app[bot] Jun 1, 2026
12719f3
Move check_hyps_inclusion out of the kernel
SkySkimmer Jun 2, 2026
29eafb7
Merge PR #22070: Store template inductive data abstracted w.r.t. temp…
coqbot-app[bot] Jun 2, 2026
29c3f60
Add a set primitive to the Range module.
ppedrot Jun 2, 2026
bc75915
Abstract the val variant of context datatypes.
ppedrot Jun 2, 2026
4b52da1
Add overlays.
ppedrot Jun 3, 2026
12fb4c3
Merge PR #22079: Avoid printing missing-scheme warning when rewrite f…
coqbot-app[bot] Jun 3, 2026
9261f52
Merge PR #22077: Reduction effects use econstr
coqbot-app[bot] Jun 3, 2026
d08bf74
Merge PR #22090: Abstract the val variant of context datatypes.
coqbot-app[bot] Jun 3, 2026
a3061af
Merge PR #22089: Add a set primitive to the Range module.
coqbot-app[bot] Jun 3, 2026
c0f0c8d
Merge PR #22087: Move check_hyps_inclusion out of the kernel
coqbot-app[bot] Jun 3, 2026
57c4d83
Parse Ltac2 matches at level 0.
rlepigre-skylabs-ai Jun 3, 2026
3e09cfe
[fix] ssrmatching/equality and univ poly handling
mattam82 May 23, 2026
81d28e6
[fix] program fixpoint not typechecking its whole construction, poten…
mattam82 Apr 8, 2026
9ef261b
[fix] program fixpoint not typechecking its whole construction, poten…
mattam82 Jun 5, 2026
7d64bf6
Make with-jobs work on OS X, where nproc is unavailable
mattam82 Jun 5, 2026
e880357
Merge PR #22098: Fix with-jobs.sh on OS X
coqbot-app[bot] Jun 5, 2026
339f78d
Merge PR #22092: Parse Ltac2 matches at level 0.
coqbot-app[bot] Jun 6, 2026
cb44bc1
Merge PR #22074: Remove more global lazys
coqbot-app[bot] Jun 8, 2026
bf9dbd4
Merge PR #22096: [fix] ssrmatching/equality and univ poly handling
coqbot-app[bot] Jun 9, 2026
2c545df
Merge PR #22097: Fix program typing bug
coqbot-app[bot] Jun 10, 2026
c2c27c3
Print the segment hash in votour toplevel output.
ppedrot Jun 7, 2026
195cc6e
Merge PR #22112: Print the segment hash in votour toplevel output.
coqbot-app[bot] Jun 10, 2026
817e561
Test case for attributes on hooks
gmalecha-at-skylabs Jun 10, 2026
b21665b
Install hooks when attributes are completed
gmalecha-at-skylabs Jun 10, 2026
7fe364c
A sketch for a hint attribute plugin
gmalecha-at-skylabs Jun 10, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
134 changes: 80 additions & 54 deletions .github/CODEOWNERS
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,21 @@

/CONTRIBUTING.md @rocq-prover/contributing-process-maintainers

.mailmap @rocq-prover/contributing-process-maintainers

CREDITS @rocq-prover/contributing-process-maintainers
LICENSE @rocq-prover/contributing-process-maintainers

########## Fallback for /dev/ ###########

/dev/ @rocq-prover/dev-tools-maintainers

########## Build system ##########

/Makefile @rocq-prover/build-maintainers
/dev/tools/make_git_revision.sh @rocq-prover/build-maintainers

/configure @rocq-prover/build-maintainers
/tools/configure/* @rocq-prover/build-maintainers

/tools/coqdep/ @rocq-prover/build-maintainers
/config/ @rocq-prover/build-maintainers

/boot/ @rocq-prover/build-maintainers

Expand Down Expand Up @@ -49,6 +55,8 @@
/doc/ @rocq-prover/doc-maintainers
/dev/doc/ @rocq-prover/doc-maintainers

*.mld @rocq-prover/doc-maintainers

/doc/changelog/*/*.rst
/dev/doc/changes.md
# Trick to avoid getting review requests
Expand Down Expand Up @@ -108,9 +116,11 @@
/kernel/vconv.* @rocq-prover/vm-native-maintainers
/kernel/genOpcodeFiles.* @rocq-prover/vm-native-maintainers

/kernel/sorts.* @rocq-prover/universes-maintainers
/kernel/uGraph.* @rocq-prover/universes-maintainers
/kernel/univ.* @rocq-prover/universes-maintainers
/kernel/sorts.* @rocq-prover/universes-maintainers
/kernel/uGraph.* @rocq-prover/universes-maintainers
/kernel/univ.* @rocq-prover/universes-maintainers
/kernel/pConstraints.* @rocq-prover/universes-maintainers
/kernel/qGraph.* @rocq-prover/universes-maintainers

########## Library ##########

Expand All @@ -124,49 +134,50 @@

########## Standard library and plugins ##########

/theories/Corelib/ @rocq-prover/stdlib-maintainers
/theories/Corelib/ @rocq-prover/stdlib-maintainers

/theories/Corelib/Classes/ @rocq-prover/typeclasses-maintainers
/theories/Corelib/Classes/ @rocq-prover/typeclasses-maintainers


/theories/Corelib/Compat/ @rocq-prover/compat-maintainers
/theories/Corelib/Compat/ @rocq-prover/compat-maintainers

/plugins/btauto/ @rocq-prover/btauto-maintainers
/plugins/btauto/ @rocq-prover/btauto-maintainers

/plugins/cc/ @rocq-prover/cc-maintainers
/plugins/cc/ @rocq-prover/cc-maintainers

/plugins/derive/ @rocq-prover/derive-maintainers
/theories/Corelib/derive/ @rocq-prover/derive-maintainers
/plugins/derive/ @rocq-prover/derive-maintainers
/theories/Corelib/derive/ @rocq-prover/derive-maintainers

/plugins/extraction/ @rocq-prover/extraction-maintainers
/theories/Corelib/extraction/ @rocq-prover/extraction-maintainers
/plugins/extraction/ @rocq-prover/extraction-maintainers
/theories/Corelib/extraction/ @rocq-prover/extraction-maintainers

/plugins/firstorder/ @rocq-prover/firstorder-maintainers
/plugins/firstorder/ @rocq-prover/firstorder-maintainers

/plugins/funind/ @rocq-prover/funind-maintainers
/plugins/funind/ @rocq-prover/funind-maintainers

/plugins/ltac/ @rocq-prover/ltac-maintainers
/plugins/ltac/ @rocq-prover/ltac-maintainers

/plugins/micromega/ @rocq-prover/micromega-maintainers
/plugins/micromega/ @rocq-prover/micromega-maintainers

/plugins/nsatz/ @rocq-prover/nsatz-maintainers
/plugins/nsatz/ @rocq-prover/nsatz-maintainers

/plugins/ring/ @rocq-prover/ring-maintainers
/plugins/ring/ @rocq-prover/ring-maintainers

/plugins/ssrmatching/ @rocq-prover/ssreflect-maintainers
/theories/Corelib/ssrmatching/ @rocq-prover/ssreflect-maintainers
/plugins/ssrmatching/ @rocq-prover/ssreflect-maintainers
/theories/Corelib/ssrmatching/ @rocq-prover/ssreflect-maintainers

/plugins/ssr/ @rocq-prover/ssreflect-maintainers
/theories/Corelib/ssr/ @rocq-prover/ssreflect-maintainers
/plugins/ssr/ @rocq-prover/ssreflect-maintainers
/plugins/ssrrewrite/ @rocq-prover/ssreflect-maintainers
/theories/Corelib/ssr/ @rocq-prover/ssreflect-maintainers

/test-suite/ssr/ @rocq-prover/ssreflect-maintainers
/test-suite/ssr/ @rocq-prover/ssreflect-maintainers

/plugins/syntax/ @rocq-prover/parsing-maintainers
/plugins/syntax/ @rocq-prover/parsing-maintainers

/plugins/rtauto/ @rocq-prover/rtauto-maintainers
/plugins/rtauto/ @rocq-prover/rtauto-maintainers

/plugins/ltac2/ @rocq-prover/ltac2-maintainers
/theories/Ltac2 @rocq-prover/ltac2-maintainers
/plugins/ltac2/ @rocq-prover/ltac2-maintainers
/theories/Ltac2 @rocq-prover/ltac2-maintainers

########## Pretyper ##########

Expand Down Expand Up @@ -198,29 +209,35 @@

########## Number ##########

/interp/numTok.* @rocq-prover/number-maintainers
/kernel/float64* @rocq-prover/number-maintainers
/kernel/uint63* @rocq-prover/number-maintainers
/plugins/syntax/g_number_string.mlg @rocq-prover/number-maintainers
/interp/numTok.* @rocq-prover/number-maintainers
/kernel/float64* @rocq-prover/number-maintainers
/kernel/uint63* @rocq-prover/number-maintainers
/plugins/syntax/g_number_string.mlg @rocq-prover/number-maintainers
/plugins/syntax/int63_syntax_plugin.mllib @rocq-prover/number-maintainers
/plugins/syntax/number.ml @rocq-prover/number-maintainers
/plugins/syntax/number.ml @rocq-prover/number-maintainers
/plugins/syntax/number_string_notation_plugin.mllib @rocq-prover/number-maintainers
/test-suite/output/*Number* @rocq-prover/number-maintainers
/test-suite/primitive/float/ @rocq-prover/number-maintainers
/test-suite/primitive/sint63/ @rocq-prover/number-maintainers
/test-suite/primitive/uint63/ @rocq-prover/number-maintainers
/theories/Corelib/Init/Decimal.v @rocq-prover/number-maintainers
/theories/Corelib/Init/Hexadecimal.v @rocq-prover/number-maintainers
/theories/Corelib/Init/Nat.v @rocq-prover/number-maintainers
/theories/Corelib/Init/Number.v @rocq-prover/number-maintainers
/theories/Corelib/Numbers/ @rocq-prover/number-maintainers
/theories/Corelib/Floats/ @rocq-prover/number-maintainers
/test-suite/output/*Number* @rocq-prover/number-maintainers
/test-suite/primitive/float/ @rocq-prover/number-maintainers
/test-suite/primitive/sint63/ @rocq-prover/number-maintainers
/test-suite/primitive/uint63/ @rocq-prover/number-maintainers
/theories/Corelib/Init/Decimal.v @rocq-prover/number-maintainers
/theories/Corelib/Init/Hexadecimal.v @rocq-prover/number-maintainers
/theories/Corelib/Init/Nat.v @rocq-prover/number-maintainers
/theories/Corelib/Init/Number.v @rocq-prover/number-maintainers
/theories/Corelib/Numbers/ @rocq-prover/number-maintainers
/theories/Corelib/Floats/ @rocq-prover/number-maintainers

########## Tools ##########

/tools/ @rocq-prover/dev-tools-maintainers

/tools/configure/* @rocq-prover/build-maintainers
/tools/coqdep/ @rocq-prover/build-maintainers

/tools/coqdoc/ @rocq-prover/coqdoc-maintainers
/test-suite/coqdoc/ @rocq-prover/coqdoc-maintainers
/tools/coqwc* @rocq-prover/coqdoc-maintainers
/tools/rocqwc* @rocq-prover/coqdoc-maintainers
/test-suite/coqwc/ @rocq-prover/coqdoc-maintainers

/tools/coq_makefile* @rocq-prover/coq-makefile-maintainers
Expand All @@ -230,14 +247,16 @@
/tools/TimeFileMaker.py @rocq-prover/coq-makefile-maintainers
/tools/make-*-tim*.py @rocq-prover/coq-makefile-maintainers

/tools/coq_tex* @silene
/tools/coq_tex* @silene
/tools/rocqtex* @silene
# Secondary maintainer @gares

########## Toplevel ##########

/toplevel/ @rocq-prover/toplevel-maintainers
/topbin/ @rocq-prover/toplevel-maintainers
/sysinit/ @rocq-prover/toplevel-maintainers
/toplevel/ @rocq-prover/toplevel-maintainers
/topbin/ @rocq-prover/toplevel-maintainers
/sysinit/ @rocq-prover/toplevel-maintainers
/dev/ml_toplevel/ @rocq-prover/toplevel-maintainers

########## Vernacular ##########

Expand All @@ -258,10 +277,17 @@

########## Developer tools ##########

/dev/tools/ @rocq-prover/dev-tools-maintainers
/dev/tools/ @rocq-prover/dev-tools-maintainers

/dev/tools/make_git_revision.sh @rocq-prover/build-maintainers

.gitattributes @rocq-prover/dev-tools-maintainers
.gitignore @rocq-prover/dev-tools-maintainers
.ocp-indent @rocq-prover/dev-tools-maintainers

########## Dune ##########

/.ocamlinit @rocq-prover/build-maintainers
*dune* @rocq-prover/build-maintainers
*.opam @rocq-prover/build-maintainers @erikmd
/.ocamlinit @rocq-prover/build-maintainers
*dune* @rocq-prover/build-maintainers
*.opam @rocq-prover/build-maintainers @Justme0606
*.opam.template @rocq-prover/build-maintainers @Justme0606
3 changes: 3 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,9 @@ result

# documentation

doc/unreleased.rst
doc/refman-html
doc/refman-pdf
doc/common/version.tex
doc/faq/html/
doc/faq/axioms.eps
Expand Down
Loading
Loading