- 15 Apr, 2016 1 commit
-
-
Ralf Jung authored
-
- 13 Apr, 2016 1 commit
-
-
Ralf Jung authored
-
- 12 Apr, 2016 3 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This reverts commit 3cc38ff6. The reverted pure hypotheses and variables appear in the wrong order.
-
Robbert Krebbers authored
-
- 11 Apr, 2016 1 commit
-
-
Robbert Krebbers authored
-
- 08 Apr, 2016 1 commit
-
-
Robbert Krebbers authored
Since strip_later is doing a good job stripping laters in the conclusion, these tactics are thus no longer needed. Also, wp_finish now properly converts the result in a primitive viewshift in case it is not a weakestpre.
-
- 29 Mar, 2016 3 commits
-
-
Robbert Krebbers authored
-
Ralf Jung authored
This required a new ectx axiom: Positivity of evaluation contexts. This axiom was also present in the old Iris 1.1 development, back when it still derived lifting axioms for ectx languages.
-
Ralf Jung authored
-
- 20 Mar, 2016 1 commit
-
-
Ralf Jung authored
-
- 10 Mar, 2016 5 commits
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Thanks to Amin Timany for the suggestion.
-
- 07 Mar, 2016 1 commit
-
-
Ralf Jung authored
Add both non-expansive and contractive functors, and bundle them for the general Iris instance as well as the global functor construction This allows us to move the \later in the user-defined functor to any place we want. In particular, we can now have "\later (iProp -> iProp)" in the ghost CMRA.
-
- 05 Mar, 2016 1 commit
-
-
Ralf Jung authored
-
- 04 Mar, 2016 1 commit
-
-
Robbert Krebbers authored
-
- 03 Mar, 2016 1 commit
-
-
Robbert Krebbers authored
-
- 02 Mar, 2016 4 commits
-
-
Ralf Jung authored
-
Robbert Krebbers authored
We no longer abuse empty strings for anonymous binders. Instead, we now have a data type for binders: a binder is either named or anonymous.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This cleans up some ad-hoc stuff and prepares for a generalization of saved propositions.
-
- 26 Feb, 2016 1 commit
-
-
Robbert Krebbers authored
It is based on type classes and can it be tuned by providing instances, for example, instances can be provided to mark that certain expressions are closed.
-
- 22 Feb, 2016 6 commits
-
-
Robbert Krebbers authored
And now the part that I forgot to commit.
-
Robbert Krebbers authored
Also, give all these global functors the suffix GF to avoid shadowing such as we had with authF. And add some type annotations for clarity.
-
Ralf Jung authored
I added a new typeclass "inGF" to witness that a particular *functor* is part of \Sigma. inG, in contrast, witnesses a particular *CMRA* to be in there, after applying the functor to "\later iProp". inGF can be inferred if that functor is consed to the head of \Sigma, and it is preserved by consing a new functor to \Sigma. This is not the case for inG since the recursive occurence of \Sigma also changes. For evry construction (auth, sts, saved_prop), there is an instance infering the respective authG, stsG, savedPropG from an inGF. There is also a global inG_inGF, but Coq is unable to use it. I tried to instead have *only* inGF, since having both typeclasses seemed weird. However, then the actual type that e.g. "own" is about is the result of applying a functor, and Coq entirely fails to infer anything. I had to add a few type annotations in heap.v, because Coq tried to use the "authG_inGF" instance before the A got fixed, and ended up looping and expanding endlessly on that proof of timelessness. This does not seem entirely unreasonable, I was honestly surprised Coq was able to infer the types previously.
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- 21 Feb, 2016 1 commit
-
-
Ralf Jung authored
this makes it slightlymore annoying to use because we have to elliminate the box. one more reason to have a proof mode ;-)
-
- 20 Feb, 2016 8 commits