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 13, 2024 — Nov 13, 2025 Showing page 3 of 1,566 Search / Filter on:
Stop exposing Indschemes.declare_congr_scheme	Gaëtan Gilbert	More...				14 days ago
Merge PR #21248: Add command "Scheme Rewriting" and use to avoid dynamically generated schemes	coqbot-app[bot]	More...				14 days ago
Fix a fast path in w_unify_to_subterm heuristic.	Pierre-Marie Pédrot	More...				14 days ago
Stop using lax retyping in get_head_kind	Gaëtan Gilbert	More...				14 days ago
Merge PR #21179: Try βδι-reducing the type shape in w_unify_to_subterm.	coqbot-app[bot]	More...				14 days ago
Stop catching async exceptions in hacks that catch anomalies	Gaëtan Gilbert	More...				14 days ago
Merge PR #21244: Fix ssrintro	coqbot-app[bot]	More...				14 days ago
Merge PR #21249: Fix test suite	coqbot-app[bot]	More...				15 days ago
Fix test suite	Gaëtan Gilbert	More...				15 days ago
Merge PR #21228: More informative "not enough abstractions in fix body" error message	coqbot-app[bot]	More...				15 days ago
Merge PR #21239: Ltac2 add some to_message APIs	coqbot-app[bot]	More...				15 days ago
Merge PR #21218: Fix Fixpoint with measure	coqbot-app[bot]	More...				15 days ago
Merge PR #21219: Fix debug printing when there are evars in a match branch	coqbot-app[bot]	More...				15 days ago
Merge PR #21221: Improved relevance handling in eqschemes	coqbot-app[bot]	More...				15 days ago
Merge PR #21242: Bring "Fixpoint" output test back from stdlib	coqbot-app[bot]	More...				15 days ago
Merge PR #21246: Bench fix skipping packages with failed dependencies with modern opam output	coqbot-app[bot]	More...				15 days ago
Bench fix skipping packages with failed dependencies with modern opam output	Gaëtan Gilbert	More...				16 days ago
Merge PR #21243: Abstract away the Evd.side_effects record type.	coqbot-app[bot]	More...				16 days ago
Merge PR #21232: add test for #9060	coqbot-app[bot]	More...				16 days ago
Add overlays.	Pierre-Marie Pédrot	More...				17 days ago
Deprecate dynamically generating schemes in tactics	Gaëtan Gilbert	More...				17 days ago
Add command "Scheme Rewriting" and use to avoid dynamically generated schemes	Gaëtan Gilbert	More...				17 days ago
Merge PR #21208: Add a cache to Dumpglob output.	coqbot-app[bot]	More...				17 days ago
Bring "Fixpoint" output test back from stdlib	Gaëtan Gilbert	More...				17 days ago
Stop "optimizing" schemes by reusing preexisting schemes in Type for other sorts	Gaëtan Gilbert	More...				17 days ago
Fix ssrintro	Pierre Roux	More...				17 days ago
changelog	Gaëtan Gilbert	More...				17 days ago
Ltac2 add Constant/Ind/Constructor/Proj.print	Gaëtan Gilbert	More...				17 days ago
Ltac2 also expose message_of_ident as Ident.print	Gaëtan Gilbert	More...				17 days ago
Ltac2 add Message.of_preterm	Gaëtan Gilbert	More...				17 days ago

←
1
2
3
4
5
6
7
8
9
…
1565
1566
→