- Jun 23, 2021
-
-
Ralf Jung authored
-
- Jun 21, 2021
-
-
Ralf Jung authored
Modes for Equiv See merge request iris/iris!701
-
- Jun 20, 2021
-
-
Ralf Jung authored
-
- Jun 19, 2021
-
-
Paolo G. Giarrusso authored
Include workaround for Coq bug #14441, and drop now-failing test for that Coq bug.
-
- Jun 18, 2021
-
-
Ralf Jung authored
Fix typos See merge request iris/iris!706
-
Paolo G. Giarrusso authored
-
Ralf Jung authored
-
Ralf Jung authored
register make_laterable as modality See merge request iris/iris!636
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
don't tie bi.weakestpre to program_logic.language (full TC approach) Closes #408 See merge request iris/iris!656
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Add mode for Dist See merge request iris/iris!700
-
Paolo G. Giarrusso authored
-
Paolo G. Giarrusso authored
-
- Jun 17, 2021
-
-
Robbert Krebbers authored
-
Ralf Jung authored
unstage max_prefix_list See merge request iris/iris!705
-
Ralf Jung authored
-
Ralf Jung authored
-
Paolo G. Giarrusso authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jun 14, 2021
-
-
Ralf Jung authored
Let `sel_pat.parse` fail with proper error when type is incorrect Closes #421 See merge request iris/iris!704
-
Robbert Krebbers authored
-
Robbert Krebbers authored
add lemmas `intuitionistic` and `intuitionistically_intro` See merge request iris/iris!703
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 13, 2021
-
-
Ralf Jung authored
-