 07 Dec, 2020 6 commits


Ralf Jung authored
Add missing `Hint Mode` for `ghost_var` and `gset_bij`; fix arguments of `gset_bijG` See merge request iris/iris!601

Robbert Krebbers authored
Also put the arguments of `gset_bijG` in the right order.

Robbert Krebbers authored

Ralf Jung authored
mono_nat_update: make first argument implicit See merge request iris/iris!600

Ralf Jung authored

Ralf Jung authored
Implement monotone partial bijections as a view See merge request iris/iris!543

 06 Dec, 2020 14 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Tej Chajed authored
This is an alternative to !91, which was written prior to views. Using the view CMRA we factor the implementation into purely algebraic library and a logiclevel wrapper. The logiclevel wrapper exports resources which seal away the underlying ownership and has theorems which handle the ownership reasoning.

Robbert authored
Rename `mnat`/`mnat_auth` into `mono_nat`. See merge request iris/iris!572

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
Remove the weaker version with the `_lb` since the stronger version is just as easy to use in the proofmode.

Robbert Krebbers authored
 This avoids confusion between `mnat` and `max_nat`. The `m` stands for `mono`.  With `_mono` added, the `_auth` suffix in the algebra name no longer makes sense, so I removed it.  This makes the names between the logic and the algebralevel library consistent.  I also renamed `_frag` into `_lb` in the algebralevel library so as to make it consistent with the logiclevel library. Furthermore make the order of lemmas consistent and make the versions for the fractions consistent.

Robbert authored
Remove `CopyDestruct` heuristic See merge request iris/iris!596

Robbert Krebbers authored

 04 Dec, 2020 14 commits


Robbert authored
add gmap_view_alloc_big See merge request iris/iris!598

Ralf Jung authored

Robbert Krebbers authored
This is an alternative to !591.

Robbert Krebbers authored

Ralf Jung authored



Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored
wp_finish: avoid making a goal unprovable See merge request iris/iris!593

Ralf Jung authored

Ralf Jung authored
Make the IPM documentation more useful See merge request iris/iris!589

 03 Dec, 2020 6 commits


Tej Chajed authored
 Separated out the simpler invocations of tactics from their full forms. In the process we now document what parts of a tactic are optional.  Convey what the common and rare tactics are, for example that the argument to `iModIntro` is rarely needed.  Use "destruct" to talk about invoking an intro pattern, rather than eliminate, to stay closer to Coq terminology and avoid this potentially confusing PL term.  Added an overview of the "grammar entries" relevant to many tactics (ipat, selpat, spat, and pm_trm). Added links to those sections everywhere.

Ralf Jung authored
Add explicit Local/Global to hints at top level See merge request iris/iris!594

Tej Chajed authored

Tej Chajed authored

Tej Chajed authored
Fixes new Coq master warning deprecatedhintwithoutlocality (https://github.com/coq/coq/pull/13188).

Ralf Jung authored
link to pinnedpackageversions page See merge request iris/iris!590
