 18 Dec, 2016 2 commits
 16 Dec, 2016 3 commits
 15 Dec, 2016 1 commit


Robbert Krebbers authored

 14 Dec, 2016 6 commits
 13 Dec, 2016 6 commits


Ralf Jung authored

Robbert Krebbers authored
This fixes the following issue by JH Jourdan: The fact of including uPred_[...] in the module uPred (in base_logic.v), implies that typeclasses instances are declared twice. Once in module uPred and once in module uPred_[...]. This has the unfortunate consequence that it has to backtrack to both instances each time the first one fails, making failure of type class search for e.g. PersistentP potentially exponential. Goal ((□ ∀ (x1 x2 x3 x4 x5: nat), True ∗ True) ∗ True : iProp Σ). Time iIntros "#H". Undo. Remove Hints uPred_derived.forall_persistent : typeclass_instances. Time iIntros "#H". Thanks to Jason Gross @ Coq club for suggesting this fix.


Ralf Jung authored

JacquesHenri Jourdan authored

JacquesHenri Jourdan authored

 12 Dec, 2016 17 commits


Robbert Krebbers authored

Robbert Krebbers authored
Also:  Remove the wp_strip_later hack.  Let wp_lam, wp_rec, wp_... initiate the proof mode.


Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored
I also renamed `iProof` into `iStartProof`, as it is supposed to be something internal, and not a substitute of Coq's `Proof` command (as originally intended).

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored
Fix a typo in constructions.tex x_1 should be a_1 See merge request !35

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

 11 Dec, 2016 1 commit


Dan Frumin authored

 09 Dec, 2016 4 commits


Ralf Jung authored

Ralf Jung authored
Really, *all* of our files contain proof rules

Ralf Jung authored
Use agree instead of dec_agree This demonstrates that a listbased agreement could work, and form an OFE. I didn't bother to prove all the functor laws. Man, this reasoning with about the lists is annoying^^. What I don't like about this is that uninjection (`agree_car`) is only nonexpansive for valid elements. I want to try using a different equivalence relation, maybe I can find one where this works. Cc @jjourdan @robbertkrebbers See merge request !22

Ralf Jung authored
Thanks to Robbert for fixing gen_heap
