Coq proof assistant

Settings | Report Duplicate

20

I Use This!

Very High Activity

Commits : Listings

Analyzed about 3 hours ago. based on code collected about 4 hours ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Nov 19, 2024 — Nov 19, 2025 Showing page 10 of 1,568 Search / Filter on:
Merge PR #21166: Get rid of level-tolerance warning levels	coqbot-app[bot]	More...				about 1 month ago
add overlay for elpi	nicolas tabareau	More...				about 1 month ago
Get rid of level-tolerance warning levels	Pierre Roux	More...				about 1 month ago
Ltac2: More forward compatible relevance API	Gaëtan Gilbert	More...				about 2 months ago
Add overlay	Pierre Roux	More...				about 2 months ago
Merge PR #21107: Add warning for non closed level 0 notations	coqbot-app[bot]	More...				about 2 months ago
Refine the notation-incompatible-prefix warning	Pierre Roux	More...				about 2 months ago
parametrize typeclass functions with the db	nicolas tabareau	More...				about 2 months ago
Merge PR #21155: Avoid declaring a parsing rule for head_of_constr	coqbot-app[bot]	More...				about 2 months ago
Merge PR #21097: Have Evd use einstance everywhere	coqbot-app[bot]	More...				about 2 months ago
Merge PR #21152: Move Optimize Proof and Optimize Heap out of ltac plugin	coqbot-app[bot]	More...				about 2 months ago
overlays	Gaëtan Gilbert	More...				about 2 months ago
Merge PR #21147: Enforcing more invariants in Ind_tables.Locmap module.	coqbot-app[bot]	More...				about 2 months ago
Merge PR #21145: Stop relying on canonical names in Detyping option API.	coqbot-app[bot]	More...				about 2 months ago
Merge PR #21143: Bubble up the imperative registering of constants in proof APIs	coqbot-app[bot]	More...				about 2 months ago
Merge PR #21140: Use user equality in comparison of native values.	coqbot-app[bot]	More...				about 2 months ago
Avoid declaring a parsing rule for head_of_constr	Gaëtan Gilbert	More...				about 2 months ago
Label some arguments of induction_gen	Gaëtan Gilbert	More...				about 2 months ago
Cache the result of node expansion of inductive guard checking.	Pierre-Marie Pédrot	More...				about 2 months ago
Merge PR #21150: Don't drop evar map in replace_using_leibniz	coqbot-app[bot]	More...				about 2 months ago
Merge PR #21148: slightly improve boxing in TC debug output	coqbot-app[bot]	More...				about 2 months ago
Move Optimize Proof and Optimize Heap out of ltac plugin	Gaëtan Gilbert	More...				about 2 months ago
Merge PR #21151: Add test for #4490	coqbot-app[bot]	More...				about 2 months ago
Add overlays	Yann Leray	More...				about 2 months ago
Add test for #4490	Gaëtan Gilbert	More...				about 2 months ago
Don't drop evar map in replace_using_leibniz	Gaëtan Gilbert	More...				about 2 months ago
Cleanup backtrace handling in timeout implementation	Gaëtan Gilbert	More...				about 2 months ago
Properly handle `Timeout x Fail cmd`	Gaëtan Gilbert	More...				about 2 months ago
Remove alias CErrors.Timeout = Control.Timeout	Gaëtan Gilbert	More...				about 2 months ago
slightly improve boxing in TC debug output	Gaëtan Gilbert	More...				about 2 months ago

←
1
2
…
6
7
8
9
10
11
12
13
14
…
1567
1568
→