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
add {fst,snd}_map_zip
!285
· created
Jun 23, 2021
by
Ralf Jung
Merged
3
updated
Jun 27, 2021
add zip_with_diag and zip_diag
!215
· created
Jan 19, 2021
by
Ralf Jung
Merged
1
updated
Jan 19, 2021
add version of Qp_lower_bound that returns less-than facts
!186
· created
Oct 01, 2020
by
Ralf Jung
Merged
1
updated
Oct 01, 2020
add unfolding lemma for bool_decide: bool_decide_decide
!73
· created
Jun 18, 2019
by
Ralf Jung
Merged
1
updated
Jun 18, 2019
Add two useful lemmas
!101
· created
Oct 31, 2019
by
Amin Timany
Merged
5
updated
Nov 01, 2019
Add the feed revert, efeed revert, efeed inversion, and efeed destruct tactics
!389
· created
Jul 26, 2022
by
Michael Sammler
Closed
20
updated
Aug 09, 2022
Add tests for equiv notation
!143
· created
Apr 09, 2020
by
Paolo G. Giarrusso
Merged
2
updated
Apr 10, 2020
add telescopic versions of the Coq quantifiers
!34
· created
Jun 09, 2018
by
Ralf Jung
Merged
24
updated
Jun 09, 2018
add telescopes and a bit of theory about them
!33
· created
Jun 05, 2018
by
Ralf Jung
Merged
54
updated
Jun 06, 2018
add target html and gallinahtml
!2
· created
Feb 17, 2017
by
Benoit Viguier
Merged
4
updated
Feb 23, 2017
Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
!352
· created
Dec 16, 2021
by
Robbert Krebbers
Merged
1
updated
Dec 16, 2021
add tactic for solving computable goals
!261
· created
May 03, 2021
by
Ralf Jung
Merged
17
updated
May 18, 2021
Add tactic `tc_solve`.
!425
· created
Nov 24, 2022
by
Robbert Krebbers
Merged
3
updated
Nov 30, 2022
Add tactic `learn_hyp`, fixes #73
!247
· created
Apr 15, 2021
by
Michael Sammler
Merged
6
updated
Apr 19, 2021
Add ssreflect file (from Iris).
!471
· created
Apr 28, 2023
by
Robbert Krebbers
Merged
3
updated
Jul 26, 2023
add some very basic f_equiv tests
!409
· created
Aug 11, 2022
by
Ralf Jung
Merged
2
updated
Aug 12, 2022
add some union_with lemmas
!432
· created
Dec 13, 2022
by
Ralf Jung
Merged
27
updated
Apr 14, 2023
Add some type annotations for prepare for `Hint Mode` for `Equiv`.
!418
· created
Oct 06, 2022
by
Robbert Krebbers
Merged
0
updated
Oct 08, 2022
add some number instances for Assoc, Comm, ...
!513
· created
Sep 27, 2023
by
Ralf Jung
Merged
5
updated
Sep 29, 2023
add some map-fmap lemmas
!489
· created
Jul 27, 2023
by
Ralf Jung
Merged
1
updated
Aug 02, 2023
Prev
1
…
15
16
17
18
19
20
21
22
23
…
28
Next