openhub.net
Black Duck Software, Inc.
Black Duck Open Hub
Follow @
OH
Sign In
Join Now
Projects
People
Organizations
Tools
Blog
BDSA
Projects
People
Projects
Organizations
Forums
Coq proof assistant
Settings
|
Report Duplicate
20
I Use This!
×
Login Required
Log in to Open Hub
Remember Me
Very High Activity
Commits
: Listings
Analyzed
about 14 hours
ago. based on code collected
1 day
ago.
Apr 17, 2024 — May 17, 2024
Showing page 1 of 5
Search / Filter on:
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...
3 days ago
Merge PR #19015: Factor the lambda compilation passes of VM and native
coqbot-app[bot]
More...
3 days ago
Update doc/tools/docgram/common.edit_mlg
Pierre Rousselin
More...
3 days ago
Merge PR #19028: Remove the Evd.sig datatype.
coqbot-app[bot]
More...
3 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...
4 days ago
additions/corrections about scopes in the refman
Pierre Rousselin
More...
4 days ago
Merge PR #19022: univminim: always use lbound:Set when adding univs to ugraph
coqbot-app[bot]
More...
4 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...
5 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
←
1
2
3
4
5
→
This site uses cookies to give you the best possible experience. By using the site, you consent to our use of cookies. For more information, please see our
Privacy Policy
Agree