Skip to content
GitLab
Explore
Sign in
Iris
stdpp
Merge requests
Open
9
Merged
493
Closed
47
All
549
Actions
Subscribe to RSS feed
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
{{title}}
Title
Random collection of lemmas from RefinedC
!244
· created
Apr 14, 2021
by
Michael Sammler
Closed
9
updated
Apr 15, 2021
readme: mention more operations we block
!544
· created
Apr 03, 2024
by
Ralf Jung
Merged
1
updated
Apr 12, 2024
Refactor and improve documentation of feed and efeed tactics
!403
· created
Aug 02, 2022
by
Michael Sammler
Merged
40
updated
Aug 16, 2022
relate size of map to size of its domain
!320
· created
Aug 11, 2021
by
Ralf Jung
Merged
3
updated
Sep 05, 2021
relations lemmas
!316
· created
Jul 28, 2021
by
Ralf Jung
Merged
11
updated
Jul 28, 2021
relations.nsteps: add inversion lemma for `nsteps R 1 a b`
!87
· created
Aug 21, 2019
by
Paolo G. Giarrusso
Merged
8
updated
Aug 23, 2019
Release 1.9.0
!516
· created
Oct 04, 2023
by
Johannes Hostert
Merged
24
updated
Oct 11, 2023
remove 'wf' alias for the standard 'well_founded'
!524
· created
Oct 14, 2023
by
Ralf Jung
Merged
7
updated
Oct 14, 2023
Remove `:>>` subclass instance declarations
!104
· created
Nov 07, 2019
by
Robbert Krebbers
Merged
0
updated
Nov 07, 2019
Remove `left associativity` of `scalar_mult` to be compatible with math-comp.
!470
· created
Apr 28, 2023
by
Robbert Krebbers
Merged
0
updated
Apr 28, 2023
Remove `map` infix in lemmas about `dom` and `filter`.
!176
· created
Jul 16, 2020
by
Robbert Krebbers
Merged
1
updated
Jul 17, 2020
remove a Global Arguments Pos.of_nat from the middle of a proof
!350
· created
Dec 12, 2021
by
Ralf Jung
Merged
3
updated
Dec 13, 2021
Remove copyright headers, update LICENCE file.
!124
· created
Mar 13, 2020
by
Robbert Krebbers
Merged
3
updated
Mar 13, 2020
Remove curry/uncurry workaround for Coq ≤ 8.13.
!446
· created
Feb 13, 2023
by
Robbert Krebbers
Merged
1
updated
Feb 13, 2023
Remove dead type classes and notations.
!197
· created
Oct 28, 2020
by
Robbert Krebbers
Merged
1
5
updated
Oct 28, 2020
Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename...
!205
· created
Jan 04, 2021
by
Robbert Krebbers
Merged
2
updated
Jan 07, 2021
Remove FIXME in `fin_map_dom`.
!483
· created
Jun 02, 2023
by
Robbert Krebbers
Merged
0
updated
Jun 02, 2023
Remove hint db and import of omega, since omega will be removed from Coq.
!216
· created
Jan 19, 2021
by
Robbert Krebbers
Merged
0
updated
Jan 19, 2021
Remove Import NPeano
!535
· created
Nov 15, 2023
by
Pierre Rousselin
Merged
8
updated
Nov 17, 2023
Remove Permutation Proper workaround that is not needed in Coq >= 8.15.
!486
· created
Jul 25, 2023
by
Robbert Krebbers
Merged
0
updated
Jul 25, 2023
Prev
1
…
18
19
20
21
22
23
24
25
26
…
28
Next