Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
Iris
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Terraform modules
Monitor
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Gaëtan Gilbert
Iris
Graph
4426f8a30ca5c6abaf9a79824557ddb11cc4b0ed
Select Git revision
Branches
1
master
default
protected
1 result
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
1
Apr
31
Mar
27
25
23
21
20
19
18
16
13
12
10
9
6
4
28
Feb
26
25
24
23
20
19
18
17
15
14
13
12
11
10
7
6
5
4
3
2
1
30
Jan
29
23
21
18
17
16
15
14
13
11
10
9
8
7
20
Dec
19
18
14
13
10
9
6
5
4
2
25
Nov
22
21
20
14
13
12
11
10
8
7
6
5
2
1
31
Oct
25
22
18
14
12
11
9
6
20
Sep
19
13
11
9
8
6
30
Aug
29
28
27
26
25
24
22
16
14
13
12
9
8
7
6
30
Jul
22
14
13
12
9
7
5
3
1
30
Jun
29
28
27
26
25
24
21
20
19
18
17
16
15
14
13
12
11
10
9
7
6
5
Merge branch 'robbert/iso' into 'master'
Some Coqdoc improvements in the OFE file.
CHANGELOG.
Make use of OFE isomorphisms in COFE solver.
Add notion of isomorphism between OFEs.
these are all functors from OFEs
mention which categories these functors map to which
Merge branch 'inj-typeclass-2' into 'master'
Revise uses of `inj` from !408 as discussed
Prove that `≡` is limit preserving.
Let `iNext` detect equalities `Next x ≡ Next y`.
Merge branch 'inj-typeclass' into 'master'
Replace explicit use of Inj instances by inj
Merge branch 'msammler/fix_drop_insert' into 'master'
drop_insert -> drop_insert_gt
Merge branch 'add-missing-proof' into 'master'
Add missing `Proof.` to sealing proofs
Merge branch 'spell-check' into 'master'
Spell check proof_guide.md
Merge branch 'sbi-eq-notation-sections' into 'master'
sbi_internal_eq: add "sections" of notation, following stdpp
Merge branch 'robbert/atomic_wp_seq_step' into 'master'
Prove stepping (i.e., non-value) version of `atomic_wp_seq`.
Merge branch 'robbert/exist_laterable' into 'master'
Prove `Laterable (∃ x, Φ x)`.
Remove redundant space.
Merge branch 'vscode-editor-docs' into 'master'
Add VS code to the editor.md docs
Merge branch 'robbert/iAssumption' into 'master'
Add documentation.
CHANGELOG entry.
Make `iAssumption` work on `⊢ ...` premises in the Coq context.
Fix errors of `iAssumption`, `iExact`, and friends.
Fix bad line break.
Instance for `Affine (□?p P)`.
update dependencies
Fix Coqdoc.
Merge branch 'ci/ralf/pair_core_id' into 'master'
Avoid slow `try done`.
change some other hints to a more general pattern and typeclass instances
Loading