 21 Dec, 2018 1 commit


Robbert Krebbers authored

 12 Dec, 2018 1 commit


Robbert Krebbers authored

 10 Dec, 2018 6 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This lemma allows one to get the witness out of a later, without having to use `later_car`, i.e. in a way that works in the onpaper version of the logic.

Robbert Krebbers authored

 08 Dec, 2018 1 commit


Robbert Krebbers authored

 03 Dec, 2018 1 commit


Robbert Krebbers authored

 29 Nov, 2018 1 commit


Tej Chajed authored
Adding a hint without a database now triggers a deprecation warning in Coq master (https://github.com/coq/coq/pull/8987).

 26 Nov, 2018 1 commit


Robbert Krebbers authored

 06 Nov, 2018 1 commit


Robbert Krebbers authored

 01 Nov, 2018 3 commits


Robbert Krebbers authored

Dan Frumin authored

Ralf Jung authored

 04 Oct, 2018 1 commit


Robbert Krebbers authored

 31 Aug, 2018 1 commit


Ralf Jung authored

 01 Aug, 2018 1 commit


Robbert Krebbers authored

 31 Jul, 2018 1 commit


Jonas Kastberg Hinrichsen authored
Added a new lemma to allocate fragmented ownership in unital gmaps while updating the full ownership

 20 Jun, 2018 1 commit


Ralf Jung authored

 29 May, 2018 2 commits
 23 May, 2018 3 commits


Robbert Krebbers authored

Robbert Krebbers authored
These results turned out to be neither that useful nor canonical, and can easily be derived from local updates. This reverts commit 465dd9f4.

Robbert Krebbers authored
Thanks to @jung for proposing these names.

 17 May, 2018 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
`sed i 's/frag_auth_op/frac_auth_frag_op/g' $(find name "*.v")`

 09 May, 2018 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 18 Apr, 2018 1 commit


Ralf Jung authored

 11 Apr, 2018 1 commit


Dan Frumin authored

 09 Apr, 2018 1 commit


JacquesHenri Jourdan authored

 05 Mar, 2018 1 commit


Ralf Jung authored
This is backwardscompatible; it desugars to a normal application on previous versions

 20 Feb, 2018 3 commits


JacquesHenri Jourdan authored
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

JacquesHenri Jourdan authored
Revert "Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type." This reverts commit fa897ff5.

JacquesHenri Jourdan authored
The finiteness was needed to have the axiom of choice over the domain. This axiom is not needed if cmra_extend is in Type.

 23 Dec, 2017 1 commit


JacquesHenri Jourdan authored

 30 Nov, 2017 1 commit


Robbert Krebbers authored
