Skip to content

Actions: artagnon/bonak

Actions

All workflows

Actions

Loading...
Loading

Showing runs from all workflows
146 workflow runs
146 workflow runs

Filter by Workflow

⌥ + click/return to exclude

Filter by Event

⌥ + click/return to exclude

Filter by Status

⌥ + click/return to exclude

Filter by Branch

⌥ + click/return to exclude

Filter by Actor

⌥ + click/return to exclude
Encode arity as Fin.t n and get rid of functional extensionality axiom rocq-action #568: Pull request #15 opened by olympichek
39m 50s olympichek:no-funext
olympichek:no-funext
39m 50s
Upgrade to Rocq 9.2 (#14) rocq-action #567: Commit 2570071 pushed by artagnon
31m 55s master
master
31m 55s
Upgrade to Rocq 9.2 rocq-action #566: Pull request #14 synchronize by olympichek
31m 7s olympichek:rocq-9.2
olympichek:rocq-9.2
31m 7s
Upgrade to Rocq 9.2 rocq-action #565: Pull request #14 synchronize by olympichek
10m 13s olympichek:rocq-9.2
olympichek:rocq-9.2
10m 13s
Upgrade to Rocq 9.2 rocq-action #564: Pull request #14 opened by olympichek
10m 20s olympichek:rocq-9.2
olympichek:rocq-9.2
10m 20s
Degeneracies in all directions (#13) rocq-action #563: Commit fa8be26 pushed by artagnon
22m 11s master
master
22m 11s
Degeneracies in all directions rocq-action #562: Pull request #13 synchronize by olympichek
21m 58s olympichek:dgn-all-directions
olympichek:dgn-all-directions
21m 58s
Degeneracies in all directions rocq-action #561: Pull request #13 opened by olympichek
2m 10s olympichek:dgn-all-directions
olympichek:dgn-all-directions
2m 10s
Redefine mkRestrPainting to have better computation rule for `q := … rocq-action #560: Commit c7d6c22 pushed by artagnon
2m 43s master
master
2m 43s
Redefine mkRestrPainting to have better computation rule for q := 0 case rocq-action #559: Pull request #12 opened by olympichek
2m 38s olympichek:mkRestrPainting-q0
olympichek:mkRestrPainting-q0
2m 38s
vDgnSet: more trivial changes rocq-action #558: Commit 0f2c2b8 pushed by artagnon
2m 27s master
master
2m 27s
vSetDgn: initial pass of trivial cleanups rocq-action #557: Commit 6864489 pushed by artagnon
2m 9s master
master
2m 9s
New construction of degeneracies (#11) rocq-action #556: Commit 5f71009 pushed by artagnon
2m 30s master
master
2m 30s
Turn νSet into a module (#10) rocq-action #555: Commit 0e45bd4 pushed by artagnon
2m 14s master
master
2m 14s
New construction of degeneracies rocq-action #554: Pull request #11 opened by olympichek
2m 14s olympichek:dgn-new
olympichek:dgn-new
2m 14s
Turn νSet into a module rocq-action #553: Pull request #10 opened by olympichek
2m 14s olympichek:νSet-module
olympichek:νSet-module
2m 14s
doc: generate coqdoc documentation rocq-action #552: Commit 40b6c73 pushed by artagnon
2m 32s doc
doc
2m 32s
pages build and deployment pages-build-deployment #23: by artagnon
37s doc
doc
37s
Updating comments for rocq doc rocq-action #551: Commit 4aa2864 pushed by herbelin
2m 40s master
master
2m 40s
doc: generate coqdoc documentation rocq-action #550: Commit 5d6fb73 pushed by artagnon
2m 16s doc
doc
2m 16s
pages build and deployment pages-build-deployment #22: by artagnon
45s doc
doc
45s
Renaming Hrq into Hr by symmetry with Hq rocq-action #549: Commit cda213d pushed by herbelin
2m 29s master
master
2m 29s
Define mkRestrPainting using term mode instead of tactic mode rocq-action #548: Pull request #9 opened by olympichek
2m 23s olympichek:mkRestrPainting-term
olympichek:mkRestrPainting-term
2m 23s
pages build and deployment pages-build-deployment #21: by artagnon
37s doc
doc
37s
pages build and deployment pages-build-deployment #20: by artagnon
32s doc
doc
32s