Open Hub
Open Hub

 Settings |  Report Duplicate

20
I Use This!
Very High Activity

Commits : Listings

Analyzed about 19 hours ago. based on code collected about 21 hours ago.
Nov 28, 2024 — Nov 28, 2025
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
Merge PR #21254: Stop catching async exceptions in hacks that catch anomalies
coqbot-app[bot]
More... 26 days ago
Slightly improve error message about bad Ltac2 constructor names
Gaëtan Gilbert
More... 26 days ago
Use Evd.is_undefined instead of Evd.is_defined in Evarutil.advance
Gaëtan Gilbert
More... 26 days ago
Merge PR #21255: Stop using lax retyping in get_head_kind
coqbot-app[bot]
More... 26 days ago
Merge PR #21258: Fix deprecation message
coqbot-app[bot]
More... 26 days ago
rework of the generation of mutual eliminator
Thomas Lamiaux
More... 26 days ago
Fix deprecation message
Pierre Roux
More... 26 days ago
declare congr scheme: check registered ref, not loaded library
Gaëtan Gilbert
More... 29 days ago
Stop exposing Indschemes.declare_congr_scheme
Gaëtan Gilbert
More... 29 days ago
Merge PR #21248: Add command "Scheme Rewriting" and use to avoid dynamically generated schemes
coqbot-app[bot]
More... 29 days ago
Fix a fast path in w_unify_to_subterm heuristic.
Pierre-Marie Pédrot
More... 29 days ago
Stop using lax retyping in get_head_kind
Gaëtan Gilbert
More... 29 days ago
Merge PR #21179: Try βδι-reducing the type shape in w_unify_to_subterm.
coqbot-app[bot]
More... 29 days ago
Stop catching async exceptions in hacks that catch anomalies
Gaëtan Gilbert
More... 29 days ago
Fix buggy windows condition and regenerate opam files
Jan Midtgaard
More... 29 days ago
Ltac2 Set support Global
Gaëtan Gilbert
More... 29 days ago
Add quickfix
Pierre Roux
More... 29 days ago
Merge PR #21244: Fix ssrintro
coqbot-app[bot]
More... 29 days ago
Merge PR #21249: Fix test suite
coqbot-app[bot]
More... 30 days ago
[intern] Allow to instrument internalization via open recursion.
Emilio Jesus Gallego Arias
More... 30 days ago
Fix test suite
Gaëtan Gilbert
More... 30 days ago
Merge PR #21228: More informative "not enough abstractions in fix body" error message
coqbot-app[bot]
More... 30 days ago
Merge PR #21239: Ltac2 add some to_message APIs
coqbot-app[bot]
More... 30 days ago
Merge PR #21218: Fix Fixpoint with measure
coqbot-app[bot]
More... about 1 month ago
Merge PR #21219: Fix debug printing when there are evars in a match branch
coqbot-app[bot]
More... about 1 month ago
Merge PR #21221: Improved relevance handling in eqschemes
coqbot-app[bot]
More... about 1 month ago
Merge PR #21242: Bring "Fixpoint" output test back from stdlib
coqbot-app[bot]
More... about 1 month ago
Merge PR #21246: Bench fix skipping packages with failed dependencies with modern opam output
coqbot-app[bot]
More... about 1 month ago
Bench fix skipping packages with failed dependencies with modern opam output
Gaëtan Gilbert
More... about 1 month ago
Merge PR #21243: Abstract away the Evd.side_effects record type.
coqbot-app[bot]
More... about 1 month ago