Select Git revision
- Branches 20
- ike/own_set_ops
- ike/own-validity-2
- ike/frame_evar∨∧_2
- ike/auth_structure_fix
- ike/own-validity
- master default protected
- ralf/dfrac_agree
- ralf/mono_nat
- ralf/mono_list
- dfrumin/iris-coq-is_closed_gset
- robbert/bi_wand_notation
- ci/ralf/frame-frac
- robbert/level
- ralf/f_equiv
- ralf/f_equiv_ho
- ralf/sprop
- robbert/into_ih_Forall
- ci/hai/siProp
- robbert/stdpp_mr281
- ci/ralf/Z_of_nat
- Tags 14
- iris-3.5.0
- iris-3.4.0
- iris-3.3.0
- iris-3.2.0
- iris-3.1.0
- iris-3.0.0
- iris-2.0
- iris-2.0-rc2
- iris-2.0-rc1
- iris-1.1
- iris-1.0
- hope-2015-coq-1
- appendix-1.0.0
- appendix-1
Compare
-
-
- Open in your IDE
- Download source code
- Download this directory
Forked from
Iris / Iris
Source project has a limited visibility.
Robbert Krebbers
authored
This avoids Coq distinguishing iProp and uPred (iResUR _) when it should not.
e9e55145
History
| Name | Last commit | Last update |
|---|---|---|
| .. | ||