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
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
Thibaut Pérami
stdpp
Graph
2f4644bf6111edf82c9def94704fd581151712dd
Select Git revision
Branches
3
coq-stdpp-1.0
master
default
protected
mraise
Tags
10
coq-stdpp-1.8.0
coq-stdpp-1.7.0
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
13 results
You can move around the graph by using the arrow keys.
Begin with the selected commit
Created with Raphaël 2.2.0
30
Nov
29
25
24
23
18
17
16
15
2
20
Oct
8
6
29
Sep
28
27
25
24
23
21
20
7
25
Aug
24
23
17
16
12
11
10
9
8
3
1
31
Jul
27
26
18
7
28
Jun
27
26
8
30
May
25
16
13
11
9
8
6
4
3
12
Apr
11
7
30
Mar
18
16
15
24
Feb
20
22
Jan
19
17
14
13
12
11
22
Dec
21
16
13
9
8
7
6
3
2
1
30
Nov
26
24
23
22
18
15
13
12
8
5
4
27
Oct
26
13
9
5
2
1
27
Sep
26
25
13
10
9
8
7
6
5
4
5
4
11
Aug
29
Jul
28
27
26
24
23
22
21
20
19
18
17
15
3
29
Jun
28
27
26
25
24
23
19
18
17
16
15
11
10
9
8
7
6
5
4
3
2
1
31
May
28
27
26
25
20
19
18
17
bump CI to Coq 8.16.1
Merge branch 'robbert/issue_161' into 'master'
Merge branch 'ralf/solve_ndisj' into 'master'
Move.
make sure this solves the goal
Apply 2 suggestion(s) to 2 file(s)
Merge branch 'robbert/tc_notypeclasses_refine' into 'master'
linebreaks
CHANGELOG entry.
Add some tests.
Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`.
add another testcase from iris.program_logic.atomic
make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y'
Use `notypeclasses refine` for `TCIf` and `TCNoBackTrack`.
Merge branch 'robbert/tc_solve' into 'master'
CHANGELOG.
Add tactic `tc_solve`.
Merge branch 'msammler/bv_simplify_fix' into 'master'
Merge branch 'robbert/set_solver_eauto' into 'master'
CHANGELOG.
Use `eauto` as default for `set_solver`.
Merge branch 'gset_to_gmap_to_list' into 'master'
fix readme and CI ordering
test Coq 8.16.0
rename lemma
remove some parentheses
Merge branch 'robbert/no_native_compiler' into 'master'
Add comment.
add gset_to_gmap_to_list
clarify that the unstable package needs a dev version
Merge branch 'msammler/coq_16748' into 'master'
Fix bitvector tests for coq#16748
Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`.
Rename wrongly named instance `uncurry5_proper'` into `uncurry4_proper'`.
Merge branch 'robbert/type_annotations' into 'master'
Add some type annotations for prepare for `Hint Mode` for `Equiv`.
More CHANGELOG.
More CHANGELOG fixing.
Fix CHANGELOG after !386.
Merge branch 'set_lemmas' into 'master'
Loading