Commits on Source (26)
-
Ralf Jung authored6aaddc70
-
Ralf Jung authored3ecd3e95
-
Ralf Jung authored25cc104d
-
Robbert Krebbers authoreda26d9ee5
-
Ralf Jung authored
Bump timeout to hopefully solve #571. Closes #571 See merge request iris/iris!1051
84ed8993 -
Robbert Krebbers authored
Remove the `*` specialization pattern. This pattern has been deprecated and a no-op since 2017. See !41.
df6ae78b -
Robbert Krebbers authored
Remove the `*` specialization pattern. See merge request iris/iris!1054
a14be4c1 -
Robbert Krebbers authoredcaf5ae2a
-
Robbert Krebbers authoredd0410021
-
Ralf Jung authored
More suggestive error message for `iInv`. See merge request iris/iris!1055
3818b339 -
Rodolphe Lepigre authoredf1313bda
-
Ralf Jung authored
Allow compiling the packages with dune. See merge request iris/iris!1056
47000dbc -
Ralf Jung authored3d7c7fd5
-
Ralf Jung authorede46e1b7d
-
e2118410
-
Robbert Krebbers authored
Add big_sep*_flip_mono' See merge request iris/iris!1053
f8546a91 -
b3e73b39
-
Ralf Jung authored
fix wp_cmpxchg_fail when points-to is in persistent context Closes #570 See merge request iris/iris!1057
7f856b61 -
Robbert Krebbers authored06f67042
-
Robbert Krebbers authored76a18ce3
-
Robbert Krebbers authoredf694cf77
-
Robbert Krebbers authoredacf66b74
-
b4f0c8ef
-
Robbert Krebbers authored
Always use magic wand in `iInduction` hypothesis See merge request iris/iris!1048
6cb68cdf -
Isaac van Bakel authoredVerifieda32469f5
-
Isaac van Bakel authoredVerified34b628e6
Showing
- .gitignore 2 additions, 0 deletions.gitignore
- .gitlab-ci.yml 8 additions, 0 deletions.gitlab-ci.yml
- CHANGELOG.md 25 additions, 0 deletionsCHANGELOG.md
- Makefile 6 additions, 0 deletionsMakefile
- Makefile.coq.local 1 addition, 1 deletionMakefile.coq.local
- _CoqProject 2 additions, 0 deletions_CoqProject
- coq-iris.opam 1 addition, 1 deletioncoq-iris.opam
- docs/dune.md 47 additions, 0 deletionsdocs/dune.md
- dune 10 additions, 0 deletionsdune
- dune-project 2 additions, 0 deletionsdune-project
- iris/bi/big_op.v 28 additions, 1 deletioniris/bi/big_op.v
- iris/dune 5 additions, 0 deletionsiris/dune
- iris/proofmode/coq_tactics.v 10 additions, 5 deletionsiris/proofmode/coq_tactics.v
- iris/proofmode/ltac_tactics.v 5 additions, 6 deletionsiris/proofmode/ltac_tactics.v
- iris/proofmode/spec_patterns.v 0 additions, 2 deletionsiris/proofmode/spec_patterns.v
- iris_deprecated/dune 5 additions, 0 deletionsiris_deprecated/dune
- iris_heap_lang/dune 5 additions, 0 deletionsiris_heap_lang/dune
- iris_heap_lang/proofmode.v 15 additions, 10 deletionsiris_heap_lang/proofmode.v
- iris_unstable/dune 5 additions, 0 deletionsiris_unstable/dune
- tests/bi.v 14 additions, 0 deletionstests/bi.v
docs/dune.md
0 → 100644
dune
0 → 100644
dune-project
0 → 100644
iris/dune
0 → 100644
iris_deprecated/dune
0 → 100644
iris_heap_lang/dune
0 → 100644
iris_unstable/dune
0 → 100644