Open Hub
Open Hub

 Settings |  Report Duplicate

20
I Use This!
Very High Activity

Commits : Listings

Analyzed 10 minutes ago. based on code collected about 1 hour ago.
Nov 27, 2024 — Nov 27, 2025
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
Use Gc.ramp_up on ocaml >= 5.4
Gaëtan Gilbert
More... 13 days ago
Merge PR #21297: Update ci/README-devs
coqbot-app[bot]
More... 13 days ago
Make the failed-abstract-certificate warning error by default.
Pierre-Marie Pédrot
More... 13 days ago
Simplify the implementation side-effect internals in Evd.
Pierre-Marie Pédrot
More... 13 days ago
Simplify the API to declare local constants.
Pierre-Marie Pédrot
More... 13 days ago
Remove Proofview.tclEFFECTS altogether.
Pierre-Marie Pédrot
More... 13 days ago
Remove dead API around Evd.side_effects.
Pierre-Marie Pédrot
More... 13 days ago
Code simplification in Tactics.with_set_strategy.
Pierre-Marie Pédrot
More... 13 days ago
Code simplification in tclABSTRACT.
Pierre-Marie Pédrot
More... 13 days ago
Simplify the implementation of tclEFFECTS.
Pierre-Marie Pédrot
More... 14 days ago
Merge PR #21294: Refine the cache check in TC search algorithm.
coqbot-app[bot]
More... 14 days ago
save_library_base fix order of file closing and removing
Gaëtan Gilbert
More... 14 days ago
Merge PR #19177: [core] Improved state protection against memprof-limits interruptions
coqbot-app[bot]
More... 14 days ago
Merge PR #21285: Delimiter args to Ltac2 constr synclass may be qualified with "delimiters"
coqbot-app[bot]
More... 14 days ago
Fix parsing warnings in test-suite
Pierre Roux
More... 14 days ago
Merge PR #21284: Reimplement abstract in a purely functional way.
coqbot-app[bot]
More... 14 days ago
Merge PR #21000: Make sure coqdep does not misinterpret "Importfoo" (fix #20984).
coqbot-app[bot]
More... 14 days ago
Merge PR #21300: Make fiat-crypto work on the bench.
coqbot-app[bot]
More... 14 days ago
Faster constant access in simpl reduction.
Pierre-Marie Pédrot
More... 14 days ago
Merge PR #21286: Add CI job using latest ocaml version (on github actions linux)
coqbot-app[bot]
More... 15 days ago
Merge PR #21276: next_name_away_with_default_using_types takes env and evar map
coqbot-app[bot]
More... 15 days ago
Merge PR #21289: Fix printing level of intuition-like tactic notations
coqbot-app[bot]
More... 15 days ago
Merge PR #21293: indschemes remove outdated comment
coqbot-app[bot]
More... 15 days ago
Merge PR #21296: Fix mod subst when ignoring inlining
coqbot-app[bot]
More... 15 days ago
Ltac2 Backtrace Compact
Gaëtan Gilbert
More... 15 days ago
Merge PR #21298: Bring test of #1844 back from stdlib
coqbot-app[bot]
More... 15 days ago
Merge PR #21266: Tac2quote.of_open_constr_expected_istype remove unused "delimiters" argument
coqbot-app[bot]
More... 15 days ago
Merge PR #21268: Remove unused print_meta_as_hole
coqbot-app[bot]
More... 15 days ago
Bring test of #1844 back from stdlib
Gaëtan Gilbert
More... 15 days ago
Stop using exceptions for flow control in solve_delta_kn
Gaëtan Gilbert
More... 15 days ago