Coq proof assistant

Settings | Report Duplicate

20

I Use This!

Very High Activity

Commits : Listings

Analyzed 1 day ago. based on code collected 1 day ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Nov 01, 2024 — Nov 01, 2025 Showing page 1 of 1,563 Search / Filter on:
Merge PR #21248: Add command "Scheme Rewriting" and use to avoid dynamically generated schemes	coqbot-app[bot]	More...				2 days ago
Merge PR #21179: Try βδι-reducing the type shape in w_unify_to_subterm.	coqbot-app[bot]	More...				2 days ago
Merge PR #21244: Fix ssrintro	coqbot-app[bot]	More...				3 days ago
Merge PR #21249: Fix test suite	coqbot-app[bot]	More...				3 days ago
Fix test suite	Gaëtan Gilbert	More...				3 days ago
Merge PR #21228: More informative "not enough abstractions in fix body" error message	coqbot-app[bot]	More...				3 days ago
Merge PR #21239: Ltac2 add some to_message APIs	coqbot-app[bot]	More...				3 days ago
Merge PR #21218: Fix Fixpoint with measure	coqbot-app[bot]	More...				3 days ago
Merge PR #21219: Fix debug printing when there are evars in a match branch	coqbot-app[bot]	More...				3 days ago
Merge PR #21221: Improved relevance handling in eqschemes	coqbot-app[bot]	More...				3 days ago
Merge PR #21242: Bring "Fixpoint" output test back from stdlib	coqbot-app[bot]	More...				3 days ago
Merge PR #21246: Bench fix skipping packages with failed dependencies with modern opam output	coqbot-app[bot]	More...				3 days ago
Bench fix skipping packages with failed dependencies with modern opam output	Gaëtan Gilbert	More...				4 days ago
Merge PR #21243: Abstract away the Evd.side_effects record type.	coqbot-app[bot]	More...				4 days ago
Merge PR #21232: add test for #9060	coqbot-app[bot]	More...				4 days ago
Add overlays.	Pierre-Marie Pédrot	More...				5 days ago
Add command "Scheme Rewriting" and use to avoid dynamically generated schemes	Gaëtan Gilbert	More...				5 days ago
Merge PR #21208: Add a cache to Dumpglob output.	coqbot-app[bot]	More...				5 days ago
Bring "Fixpoint" output test back from stdlib	Gaëtan Gilbert	More...				5 days ago
Fix ssrintro	Pierre Roux	More...				5 days ago
changelog	Gaëtan Gilbert	More...				5 days ago
Ltac2 add Constant/Ind/Constructor/Proj.print	Gaëtan Gilbert	More...				5 days ago
Ltac2 also expose message_of_ident as Ident.print	Gaëtan Gilbert	More...				5 days ago
Ltac2 add Message.of_preterm	Gaëtan Gilbert	More...				5 days ago
Abstract away the Evd.side_effects record type.	Pierre-Marie Pédrot	More...				5 days ago
Merge PR #21222: Ltac2 add Control.solve_constraints	coqbot-app[bot]	More...				5 days ago
Merge PR #21159: Refine the notation-incompatible-prefix warning	coqbot-app[bot]	More...				6 days ago
add test for #9060	Gaëtan Gilbert	More...				6 days ago
Merge PR #21230: Update doc of Strict Universe Declaration	coqbot-app[bot]	More...				6 days ago
Merge PR #21229: Univ poly doc: dowgrade header level of printing universes	coqbot-app[bot]	More...				6 days ago

←
1
2
3
4
5
6
7
8
9
…
1562
1563
→