Open Hub
Black Duck Open Hub

 Settings |  Report Duplicate

20
I Use This!
Very High Activity

Commits : Listings

Analyzed about 11 hours ago. based on code collected 1 day ago.
May 17, 2023 — May 17, 2024
Commit Message Contributor Files Modified Lines Added Lines Removed Code Location Date
Merge PR #18915: Fixes #11766 and #11988: restrict universes in obligations
coqbot-app[bot]
More... 1 day ago
Merge PR #18956: Do not rely on floating universes in the upper layers
coqbot-app[bot]
More... 1 day ago
Merge PR #18714: Ltac2 `assert` scope: intern and typecheck types as types
coqbot-app[bot]
More... 1 day ago
Merge PR #18641: Ltac2: warn on unused variables
coqbot-app[bot]
More... 1 day ago
Merge PR #18970: Cleanup counter handling in newprofile
coqbot-app[bot]
More... 2 days ago
Merge PR #18981: Support syntax `Type@{q | _}`
coqbot-app[bot]
More... 2 days ago
Merge PR #19021: Faster composed module substitution of terms.
coqbot-app[bot]
More... 2 days ago
Merge PR #18983: Add Fixpoint and CoFixpoint in Search logical_kind
coqbot-app[bot]
More... 2 days ago
Merge PR #18743: Making `Theorem with` more flexible + code cleanup
coqbot-app[bot]
More... 2 days ago
Merge PR #19015: Factor the lambda compilation passes of VM and native
coqbot-app[bot]
More... 2 days ago
Update doc/tools/docgram/common.edit_mlg
Pierre Rousselin
More... 2 days ago
Merge PR #19028: Remove the Evd.sig datatype.
coqbot-app[bot]
More... 2 days ago
Merge PR #18941: autobuild .merlin files in CI scripts for some plugins
coqbot-app[bot]
More... 3 days ago
Merge PR #19019: Add convenience API Sorts.make taking quality and universe
coqbot-app[bot]
More... 3 days ago
Merge PR #19020: Compatibility of new fast "make report" with MacOS X
coqbot-app[bot]
More... 3 days ago
Remove the Evd.sig datatype.
Pierre-Marie Pédrot
More... 3 days ago
Merge PR #19025: additions/corrections about scopes in the refman
coqbot-app[bot]
More... 3 days ago
additions/corrections about scopes in the refman
Pierre Rousselin
More... 3 days ago
Merge PR #19022: univminim: always use lbound:Set when adding univs to ugraph
coqbot-app[bot]
More... 3 days ago
Merge PR #19016: Automatically register induction schemes from Scheme
coqbot-app[bot]
More... 4 days ago
Merge PR #18998: [declare] Call interp_proof_using only once per mutual block.
coqbot-app[bot]
More... 4 days ago
univminim: always use lbound:Set when adding univs to ugraph
Gaëtan Gilbert
More... 4 days ago
Merge PR #19018: Bench: print size diff in vosize.log
coqbot-app[bot]
More... 4 days ago
Compatibility of new "make report" with MacOS X.
Hugo Herbelin
More... 5 days ago
Fixes #11766 and #11902: restrict universes in obligations.
Hugo Herbelin
More... 5 days ago
Declare.ml: common universe policy for auto, manual, and admitted obligations.
Hugo Herbelin
More... 5 days ago
Declare.ml: code factorisation in obligation terminators.
Hugo Herbelin
More... 5 days ago
Declare.ml: prepare obligation_admitted_terminator to provide its own uctx.
Hugo Herbelin
More... 5 days ago
Declare.ml: simplification in obligation_admitted_terminator.
Hugo Herbelin
More... 5 days ago
Add a cache for module substitution of terms.
Pierre-Marie Pédrot
More... 5 days ago