Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
2417388
νDgnSet: work in progress on degeneracies in all directions
olympichek Mar 1, 2026
1672320
νDgnSet: the type of coh-below-inf for paintings
olympichek Mar 1, 2026
b12e8bf
νDgnSet: prove coh-below-id for paintings
olympichek Mar 1, 2026
47ac0b0
νDgnSet: types of coh-below-sup and coh-above-sup for paintings
olympichek Mar 1, 2026
3f65c59
νDgnSet: prove coh-below-inf for frames
olympichek Mar 1, 2026
9b55cb5
νDgnSet: prove coh-below-sup for frames
olympichek Mar 1, 2026
ac7f9fb
νDgnSet: move coh-below-sup for frames to `DepsReflCohs2`
olympichek Mar 1, 2026
0c5fced
νDgnSet: work in progress on coh-above-sup for frames
olympichek Mar 5, 2026
d7f1e4d
νDgnSet: debugging coh-above-sup for layers
olympichek Mar 5, 2026
39022c5
νDgnSet: finish the proof of coh-above-sup for frames
olympichek Mar 5, 2026
606d6ab
νDgnSet: prove coh-below-inf for paintings
olympichek Mar 6, 2026
225fe51
νDgnSet: work in progress on coh-below-sup for paintings
olympichek Mar 6, 2026
26fc801
νDgnSet: clean-up in coh-id for layers
olympichek Mar 11, 2026
f95adcd
νDgnSet: prove coh-below-sup for paintings
olympichek Mar 11, 2026
682d3ab
νDgnSet: work in progress on coh-above-sup for paintings
olympichek Mar 11, 2026
8c3c3a9
νDgnSet: prove coh-above-sup for paintings
olympichek Mar 13, 2026
64f1cf5
νDgnSet: simplify coh-below-sup for paintings
olympichek Mar 13, 2026
dc6920d
νDgnSet: restructure refl-painting-below and simplify coh-below-sup f…
olympichek Mar 14, 2026
6c11743
νDgnSet: simplify coh-above-sup for paintings
olympichek Mar 14, 2026
b68f907
νDgnSet: rename deps objects
olympichek Mar 15, 2026
e6ecc61
νDgnSet: merge l' and c in coh-above-sup for layers
olympichek Mar 15, 2026
bb6c731
νDgnSet: prove coh-refl-refl for frames-below
olympichek Mar 15, 2026
c8fb995
νDgnSet: various simplifications
olympichek Mar 19, 2026
70b4b39
νDgnSet: prove coh-refl-refl for frames-above
olympichek Mar 19, 2026
8196df7
νDgnSet: include refl-refl coherences in `DepsReflCohs2`
olympichek Mar 20, 2026
a7d1c9a
νDgnSet: work in progress on coh-refl-refl for paintings-above
olympichek Mar 20, 2026
b339e30
νDgnSet: various simplifications
olympichek Mar 27, 2026
4c7c07a
νDgnSet: prove coh-refl-refl for paintigns-below
olympichek Mar 27, 2026
6a6bd3c
νDgnSet: add assumption for refl-refl coherence for `L`
olympichek Mar 28, 2026
78fa19a
νDgnSet: prove refl-refl coherences in 3 stages
olympichek Apr 5, 2026
41b1d3e
νDgnSet: assemble everything together
olympichek Apr 7, 2026
7a35e79
νDgnSet: ensure compatibility with upstream Rocq
olympichek Apr 7, 2026
fb008db
νDgnSet: some simplifications in proofs
olympichek Apr 7, 2026
a0389a1
νDgnSet: rename `L` to `R` to match notation in the paper
olympichek Apr 8, 2026
4563454
νDgnSet: don't unfold `leR` in examples
olympichek Apr 8, 2026
0840e7d
νDgnSet: better reduction rules, cleaner proofs, UIPs reduced from 17…
olympichek Apr 13, 2026
547521f
νDgnSet: rename id-refl-restr to id-restr-refl to match the statement
olympichek Apr 16, 2026
e5d3b66
ci: pin Rocq to 9.1.1
olympichek Apr 26, 2026
6f4eb1c
ci: trigger Rocq workflow on build config changes
olympichek Apr 26, 2026
88a1b7f
ci: trigger on synchronize event
olympichek Apr 26, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 14 additions & 3 deletions .github/workflows/coq-action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,20 @@ name: coq-action

on:
push:
paths: "**.v"
paths:
- "**.v"
- "bonak.opam"
- "dune-project"
- "**/dune"
- ".github/workflows/coq-action.yml"
pull_request:
types: [opened, reopened]
types: [opened, reopened, synchronize]
paths:
- "**.v"
- "bonak.opam"
- "dune-project"
- "**/dune"
- ".github/workflows/coq-action.yml"
jobs:
build:
runs-on: "ubuntu-latest"
Expand All @@ -16,4 +27,4 @@ jobs:
uses: "coq-community/docker-coq-action@v1"
with:
opam_file: "bonak.opam"
coq_version: "latest"
coq_version: "9.1.1"
Loading
Loading