Coq proof assistant

Settings | Report Duplicate

20

I Use This!

Very High Activity

Commits : Listings

Analyzed about 7 hours ago. based on code collected about 8 hours ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Dec 01, 2024 — Dec 01, 2025 Showing page 1 of 1,574 Search / Filter on:
Merge PR #21379: Properly declare side-effects in (some) non-proof declarations.	coqbot-app[bot]	More...				about 15 hours ago
Merge PR #21373: Uniformize exact hint resolution with others in eauto.	coqbot-app[bot]	More...				about 15 hours ago
Merge PR #21374: Small clean up around pf_ids_of_hyps in ssr tactics.	coqbot-app[bot]	More...				about 15 hours ago
Merge PR #21375: Deprecate the Tacticals.elimination_sort_of_* functions.	coqbot-app[bot]	More...				about 15 hours ago
Merge PR #21376: Add a test for bug #3608.	coqbot-app[bot]	More...				about 15 hours ago
Properly declare side-effects in non-proof declarations.	Pierre-Marie Pédrot	More...				3 days ago
Merge PR #21372: Stop exposing PrintingFlags.raw_print	coqbot-app[bot]	More...				3 days ago
Make side-effects globals to the proof block that generated them in Declare.	Pierre-Marie Pédrot	More...				4 days ago
Use a proper record for Declare.closed_proof_output type.	Pierre-Marie Pédrot	More...				4 days ago
Add a test for bug #3608.	Pierre-Marie Pédrot	More...				4 days ago
Merge PR #21371: Tweak eq_scheme_name to make HoTT backwards compatible	coqbot-app[bot]	More...				4 days ago
Deprecate the Tacticals.elimination_sort_of_* functions.	Pierre-Marie Pédrot	More...				4 days ago
Small clean up around pf_ids_of_hyps in ssr tactics.	Pierre-Marie Pédrot	More...				4 days ago
Uniformize exact hint resolution with others in eauto.	Pierre-Marie Pédrot	More...				4 days ago
Merge PR #21193: Use the same code for TC exact resolution as other hint kinds.	coqbot-app[bot]	More...				4 days ago
Stop exposing PrintingFlags.raw_print	Gaëtan Gilbert	More...				4 days ago
Merge PR #21347: Procq APIs support ignoring keyword effects, use for SSR instead of ufreezing	coqbot-app[bot]	More...				4 days ago
Merge PR #21342: Stop directly checking Printing All while printing constr	coqbot-app[bot]	More...				4 days ago
Merge PR #21370: Fix "try rewrite" not catching "missing-scheme" error	coqbot-app[bot]	More...				4 days ago
Merge PR #21369: Deprecate a good chunk of the Tacmach API	coqbot-app[bot]	More...				4 days ago
Merge PR #21365: Declaremods: remove staging compatibility layer	coqbot-app[bot]	More...				4 days ago
make more generic eq_scheme_name	nicolas tabareau	More...				4 days ago
Fix "try rewrite" not catching "missing-scheme" error	Gaëtan Gilbert	More...				5 days ago
Add changelog.	Pierre-Marie Pédrot	More...				5 days ago
Add overlays.	Pierre-Marie Pédrot	More...				5 days ago
Merge PR #21343: Print on non primitive record always prints as record	coqbot-app[bot]	More...				5 days ago
Merge PR #21098: Add a generic mechanism for rewriting with any equality satisfying J	coqbot-app[bot]	More...				5 days ago
Deprecate Tacmach.pf_last_hyp.	Pierre-Marie Pédrot	More...				5 days ago
Reduce the usage of pf_apply.	Pierre-Marie Pédrot	More...				5 days ago
Merge PR #21363: Fix elimination check in check_elim of indrec.ml	coqbot-app[bot]	More...				5 days ago

←
1
2
3
4
5
6
7
8
9
…
1573
1574
→