Skip to content
GitLab
Explore
Sign in
Iris
Iris
Merge requests
Open
20
Merged
909
Closed
118
All
1,047
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
test
!683
· created
May 20, 2021
by
Ralf Jung
Closed
1
updated
May 20, 2021
The plausibly modality
0 of 4 checklist items completed
!185
· created
Oct 27, 2018
by
Robbert Krebbers
Closed
11
updated
Jan 17, 2019
The Tactic Notation entry simple_intropattern now binds to Coq simple_intropattern.
!260
· created
Jun 08, 2019
by
Hugo Herbelin
Closed
6
updated
Jun 11, 2019
Use `class_apply` instead of `refine` to avoid unwanted evars
!342
· created
Dec 12, 2019
by
Maxime Dénès
Closed
4
updated
Dec 12, 2019
Use a smart constructor to build dfrac
!534
· created
Oct 06, 2020
by
Tej Chajed
Closed
1
18
updated
Oct 09, 2020
Use class `IntoFUpd` in tactic `wp_value_head`
!613
· created
Jan 05, 2021
by
Robbert Krebbers
S-waiting-for-author
Closed
13
updated
Dec 12, 2021
Use ⊊ instead of ⊂.
!28
· created
Nov 22, 2016
by
Jacques-Henri Jourdan
Closed
1
3
updated
Nov 25, 2016
when the goal is an evar, pick emp when possible
!139
· created
Apr 20, 2018
by
Ralf Jung
gen_proofmode
Closed
2
updated
Jan 31, 2020
WIP Define persistently from the BI interface.
!132
· created
Mar 21, 2018
by
Joseph Tassarotti
gen_proofmode
A-theory
Closed
26
updated
May 31, 2020
WIP ltac_tactics.v show `lazy_tc` does not work
!272
· created
Jun 15, 2019
by
Paolo G. Giarrusso
Closed
2
updated
Jun 18, 2019
WIP: A library for (monotone) partial bijections.
!91
· created
Nov 27, 2017
by
Dan Frumin
Closed
12
updated
Dec 18, 2020
WIP: Add `with M` option to `iModIntro` and use to redefine `iNext` to fix issue #331
!467
· created
Jun 29, 2020
by
Robbert Krebbers
S-waiting-for-author
Closed
41
updated
Sep 29, 2020
WIP: Add mk_sync
!4
· created
Aug 12, 2016
by
Ghost User
Closed
12
updated
Aug 27, 2016
WIP: Add persistent points-to predicate to Iris
!493
· created
Aug 23, 2020
by
Simon Friis Vindum
Closed
26
updated
Oct 26, 2020
WIP: add sections for ASCII notations
!426
· created
Apr 15, 2020
by
Paolo G. Giarrusso
Closed
4
updated
Jun 23, 2020
WIP: Add treiber's stack
!10
· created
Sep 12, 2016
by
Ghost User
Closed
23
updated
Oct 11, 2016
WIP: Avoid inG when possible
!219
· created
Feb 20, 2019
by
Ralf Jung
Closed
23
updated
Dec 07, 2020
WIP: Changing the definition of contractiveness to be compatible with Transfinite Iris
!616
· created
Jan 11, 2021
by
Simon Spies
S-draft
Closed
43
updated
Nov 30, 2021
WIP: Define bupd in terms of other connectives.
!172
· created
Aug 17, 2018
by
Joseph Tassarotti
Closed
11
updated
Jan 17, 2019
WIP: Define more uPred connectives in siProp
!710
· created
Jun 29, 2021
by
Hai Dang
S-draft
S-waiting-for-author
Closed
55
updated
Nov 30, 2021
Prev
1
2
3
4
5
6
Next