Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
S
stdpp
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
Environments
Terraform modules
Monitor
Incidents
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
Glen Mével
stdpp
Graph
a4fe5037d34ec7daea0ebcccc87746afa8f8a304
Select Git revision
Branches
13
coq-stdpp-1.0
glen/finite-nodec
master
default
protected
msammler/bitvector
msammler/bool_decide_simpl_never
ralf/hint-mode-check
robbert/cbn
robbert/f_equiv_pointwise
robbert/from_option
robbert/map_filter_True_False
robbert/multiset_singleton
robbert/tc_opaque
tchajed/stdpp-sprop-gmap
Tags
8
coq-stdpp-1.6.0
coq-stdpp-1.5.0
coq-stdpp-1.4.0
coq-stdpp-1.3.0
coq-stdpp-1.2.1
coq-stdpp-1.2.0
coq-stdpp-1.1.0
coq-stdpp-1.0.0
21 results
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
18
Jun
14
10
9
7
6
5
30
May
29
28
24
23
14
9
27
Apr
24
21
18
11
10
9
6
5
3
28
Mar
27
22
21
8
6
23
Feb
22
21
19
16
15
13
12
9
8
3
2
31
Jan
25
23
14
13
12
10
19
Dec
18
17
8
5
4
29
Nov
28
22
21
20
18
16
12
11
9
3
1
31
Oct
28
27
24
20
19
18
17
16
13
10
9
7
6
29
Sep
28
27
26
24
21
20
19
18
17
8
6
2
22
Aug
17
8
2
5
Jul
26
Jun
30
May
25
1
Apr
20
Mar
17
16
15
14
11
9
8
1
23
Feb
22
19
16
15
14
13
10
9
7
6
4
3
31
Jan
9
Dec
8
6
5
29
Nov
24
23
22
21
20
19
18
17
16
15
10
7
27
Oct
13
4
3
28
Sep
27
21
20
14
9
29
Aug
24
22
19
17
8
4
2
1
27
Jul
25
23
22
20
12
11
5
3
1
30
Jun
26
23
18
14
1
31
May
30
29
27
23
4
29
Apr
13
11
7
30
Mar
29
23
22
21
11
10
5
4
3
2
27
Feb
26
25
24
23
22
21
20
19
17
16
15
14
13
11
10
9
8
4
2
1
27
Jan
22
20
18
16
14
12
4
22
Dec
21
15
11
8
4
20
Nov
19
18
17
16
11
3
Feb
1
10
Jun
5
2
21
May
22
Apr
16
15
Mar
2
25
Feb
24
16
13
8
1
30
Jan
29
27
25
23
Dec
18
16
23
Nov
15
6
9
Oct
8
6
2
30
Sep
25
16
13
12
6
3
generalize ndisj_subseteq_difference to work for all masks
Merge branch 'ralf/solve_ndisj' into 'master'
solve_ndisj: try harder
Misc result about Qp.
add format specifier tp single-symbol notation
Merge branch 'ralf/telescopes' into 'master'
Teach typeclass resolution to make progress on telescopic binders
Fix universe inconsistency in Iris by making telescopes universe polymorphic
add telescopic versions of the Coq quantifiers
rename lemmas about telescope function space to tele_fun_*
Merge branch 'ralf/telescopes' into 'master'
also provide a composition for the function space
show that tele_app ∘ tele_bind is an identity; remove unused strange fmap instance
add telescopes and a bit of theory about them
.gitignore
update CI and Makefile
Merge branch 'ralf/default' into 'master'
coqdoc
introduce [default] as abbreviation for [from_option id], and use it
Merge branch 'ralf/default' into 'master'
Remove the `default` notation for options
Misc results about `Qp` fractions.
Literals 2, 3, and 4 for `Qp`.
Prove `m ∖ m = ∅` for finite maps.
update CI/Makefile
Some forgotten occurences of only parsing.
Get rid of fix/cofix without a name; these are deprecated in Coq 8.8.
update CI
solve_proper_unfold: support functions with more arguments
f_equiv: recognize 2-level pointwise_relation
update CI
re-publish opam package
test against Coq 8.8.0; update CI
`Equivalence` for `≡` on gmultisets.
Merge branch 'master' into 'master'
`Equiv` instance for multisets.
Consistent and higher precedence for default [Equiv] instances on maps/collections.
Merge branch 'robbert/rel_disambig' into 'master'
Notation `≡ₚ@{A}`.
Notation `⊑@{A}`.
Loading