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
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Model registry
Operate
Environments
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
Maxime Dénès
stdpp
Graph
6117c3e4a57307fd374780836a130ac86608d8cd
Select Git revision
Branches
16
ci/artifacts
ci/buildcache
ci/coqdoc
ci/debug
ci/opam2
ci/perf
ci/ralf/mangled
coq-stdpp-1.0
fix-export
instance-nobody-open-proof
master
default
protected
options
ralf/exact_vm_cast
ralf/notation
robbert/map_seq
robbert/set_rename
Tags
2
coq-stdpp-1.1.0
coq-stdpp-1.0.0
18 results
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
28
Jun
27
26
25
21
20
18
14
2
30
May
26
25
21
17
15
12
10
9
8
4
3
30
Apr
26
25
24
19
26
Mar
16
15
14
6
4
3
1
28
Feb
23
22
21
20
17
13
10
7
6
1
29
Jan
28
25
24
19
13
11
19
Dec
16
15
14
12
3
30
Nov
28
26
22
20
12
11
10
9
8
4
1
30
Oct
29
17
15
7
4
30
Sep
18
1
Aug
23
Jul
17
10
30
Jun
29
28
25
23
21
20
18
14
10
9
7
6
5
30
May
29
28
24
23
14
9
27
Apr
24
21
19
18
11
10
9
6
5
3
28
Mar
27
22
21
8
6
1
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
SeqZ Function
Prove `Sorted_reverse`.
Put fmap sorting lemmas in a section.
Merge branch 'robbert/involutive' into 'master'
Merge branch 'ci/robbert/naive_solver' into 'master'
Merge branch 'feature/permutation_proper' into 'master'
Define `Involutive` in terms of `Cancel`.
added two proper instance with permutations
Perform `fast_done` first in `naive_solver`.
`SetUnfold` instances for `reverse` and `fmap` on lists.
Equalities for `list_merge` with `[]` arguments.
Add class `Involutive`.
Merge branch 'ralf/proper-dom' into 'master'
show a Proper instance for dom
Add `proj1_ex` and `proj2_ex` when ∃ over `Prop`.
Merge branch 'ralf/solve_ndisj' into 'master'
coqdoc++
more generalization of lemmas and a few comments for [solve_ndisj]
move some general set lemmas to sets.v; organize ndisj hints a bit
make solve_ndisj more powerful
fix ref tests for Coq 8.10+
test solve_ndisj a bit
Merge branch 'ralf/bool_decide' into 'master'
add unfolding lemma for bool_decide: bool_decide_decide
Merge branch 'robbert/vector' into 'master'
Some missing results about vectors.
Add lemma `vec_to_list_replicate`.
Infinite docs: mention the generic constructions that should usually be used
Add `set_fold_ind_L`.
`max` and `min` infix notations for `N` and `Z` like we have for `nat`.
comment normalization
_CoqProject formatting
test 8.9.1, no longer test 8.7.0, 8.7.1
Merge branch 'inh-string' into 'master'
Merge branch 'fix-typo-instance-name' into 'master'
Strings are inhabited
Fix typo in instance name
test 8.10 beta branch
treat API pipelines like schedules and triggers
Another attempt at a `RelDecision` instance for `flip`.
Loading