Coq proof assistant

Settings | Report Duplicate

20

I Use This!

Very High Activity

Commits : Listings

Analyzed about 20 hours ago. based on code collected 1 day ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Jul 08, 2025 — Jul 08, 2026 Showing page 1 of 1,621 Search / Filter on:
Merge PR #22188: clib/hashset.ml micro-optimization ported from ocaml/stdlib/weak.ml	coqbot-app[bot]	More...				2 days ago
Merge PR #22223: Use empty variants for `Util.Empty`	coqbot-app[bot]	More...				2 days ago
Merge PR #22182: clear do not unshelve shelved evars	coqbot-app[bot]	More...				2 days ago
Use empty variants for Util.Empty	Dario Halilovic	More...				2 days ago
Merge PR #22209: Fix Search confusing is:Hypothesis and is:Axiom	coqbot-app[bot]	More...				2 days ago
Merge PR #22218: Fix small typos in Ltac2 docs	coqbot-app[bot]	More...				2 days ago
Merge PR #22207: Implement `{\| foo with fields \|}` for terms	coqbot-app[bot]	More...				3 days ago
Merge PR #22216: turn off async proofs for all output tests	coqbot-app[bot]	More...				3 days ago
Merge PR #22217: Expose open recursion more in constrintern	coqbot-app[bot]	More...				3 days ago
add overlay	CalosciMatteo	More...				3 days ago
changelog + overlay	Gaëtan Gilbert	More...				3 days ago
Fix small typos in Ltac2 docs	Dario Halilovic	More...				3 days ago
Merge PR #22210: Add MLtac2 to CI	coqbot-app[bot]	More...				3 days ago
Expose open recursion more in constrintern	Gaëtan Gilbert	More...				3 days ago
turn off async proofs for all output tests	Gaëtan Gilbert	More...				4 days ago
Merge PR #22206: changed \|= to \| when displaying universes constraints	coqbot-app[bot]	More...				4 days ago
Merge PR #22123: Deprecate non boolean if syntax	coqbot-app[bot]	More...				6 days ago
Merge PR #22169: [ssr] Fix #22158 using generalization up-to universes	coqbot-app[bot]	More...				6 days ago
Merge PR #22214: Fix test suite	coqbot-app[bot]	More...				6 days ago
Apply suggestions from code review	Gaëtan Gilbert	More...				6 days ago
Merge PR #22150: Reduce definitional UIP pattern matching when the global return type is convertible with the type in the (unique) branch	coqbot-app[bot]	More...				6 days ago
changed \|= to \| when displaying universes constraints	cecilemarcon	More...				6 days ago
Fix test suite	Gaëtan Gilbert	More...				6 days ago
Merge PR #22035: cbn: use delayed substitution	coqbot-app[bot]	More...				6 days ago
Merge PR #22189: Add missing substitution in cbv for case iv	coqbot-app[bot]	More...				6 days ago
Merge PR #22184: Add support for `autorewrite <-`	coqbot-app[bot]	More...				7 days ago
Update ci-mltac2 to apply suggestions	Dario Halilovic	More...				7 days ago
Merge PR #22194: Add (more) location information to notations.	coqbot-app[bot]	More...				7 days ago
Add MLtac2 to CI	Dario Halilovic	More...				7 days ago
Fix Search Kind Bug	CalosciMatteo	More...				7 days ago

←
1
2
3
4
5
6
7
8
9
…
1620
1621
→