Coq proof assistant

Settings | Report Duplicate

20

I Use This!

Very High Activity

Commits : Listings

Analyzed about 21 hours ago. based on code collected about 22 hours ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Nov 11, 2024 — Nov 11, 2025 Showing page 1 of 82 Search / Filter on:
Merge PR #21282: Actually save _build_ci on master	coqbot-app[bot]	More...				2 days ago
Merge PR #21287: Make the Genredexpr.red_expr_gen type open-ended.	coqbot-app[bot]	More...				2 days ago
Merge PR #21241: Stop "optimizing" schemes by reusing preexisting schemes in Type for other sorts	coqbot-app[bot]	More...				2 days ago
Add overlays.	Pierre-Marie Pédrot	More...				3 days ago
Merge PR #21231: Rewrite doc of template polymorphism	coqbot-app[bot]	More...				5 days ago
Merge PR #21103: Show diffs in Show, Show n and Show Diffs ident commands (for Proof General)	coqbot-app[bot]	More...				5 days ago
Merge PR #21267: Label boolean args of in_patargs in constrintern	coqbot-app[bot]	More...				5 days ago
Merge PR #21278: detype_rel_context is always called with "where" arg = None	coqbot-app[bot]	More...				5 days ago
Make the Genredexpr.red_expr_gen type open-ended.	Pierre-Marie Pédrot	More...				5 days ago
Merge PR #21265: Ltac2 factorize declaration of constr syntax classes	coqbot-app[bot]	More...				5 days ago
Merge PR #21245: Deprecate dynamically generating schemes in tactics	coqbot-app[bot]	More...				5 days ago
Merge PR #21270: Stop exposing Vernacentries.allow_sprop_opt_name	coqbot-app[bot]	More...				5 days ago
Merge PR #21279: Remove unused type Evd.open_constr and dead code APIs on it	coqbot-app[bot]	More...				5 days ago
Merge PR #21277: Make Constrextern.extern_env a record instead of tuple	coqbot-app[bot]	More...				5 days ago
Actually save _build_ci on master	Gaëtan Gilbert	More...				6 days ago
Merge PR #21262: Always save _build_ci on master	coqbot-app[bot]	More...				6 days ago
Remove unused type Evd.open_constr and dead code APIs on it	Gaëtan Gilbert	More...				7 days ago
detype_rel_context is always called with "where" arg = None	Gaëtan Gilbert	More...				7 days ago
Rename "vars : extern_env" argument of Constrextern.extern to "eenv"	Gaëtan Gilbert	More...				7 days ago
Make Constrextern.extern_env a record instead of tuple	Gaëtan Gilbert	More...				7 days ago
Merge PR #21220: Fix internalization of Ltac2 Notation	coqbot-app[bot]	More...				7 days ago
Merge PR #21212: Remove useless match in Evarutil.advance	coqbot-app[bot]	More...				7 days ago
Merge PR #21257: declare congr scheme: check registered ref, not loaded library	coqbot-app[bot]	More...				7 days ago
Stop exposing Vernacentries.allow_sprop_opt_name	Gaëtan Gilbert	More...				8 days ago
Merge PR #21260: Slightly improve error message about bad Ltac2 constructor names	coqbot-app[bot]	More...				8 days ago
Label boolean args of in_patargs in constrintern	Gaëtan Gilbert	More...				8 days ago
Ltac2 factorize declaration of constr syntax classes	Gaëtan Gilbert	More...				8 days ago
Merge PR #21256: Refine the fast path in w_unify_to_subterm	coqbot-app[bot]	More...				8 days ago
Merge PR #21261: Remove unused type variable	coqbot-app[bot]	More...				8 days ago
Always save _build_ci on master	Gaëtan Gilbert	More...				9 days ago

←
1
2
3
4
5
6
7
8
9
…
81
82
→