 27 Jul, 2016 1 commit


Robbert Krebbers authored
This makes type checking more directed, and somewhat more predictable. On the downside, it makes it impossible to declare the singleton on lists as an instance of SingletonM and the insert and alter operations on functions as instances of Alter and Insert. However, these were not used often anyway.

 20 Jul, 2016 1 commit


JacquesHenri Jourdan authored
* Values are considered as atomic expressions (this does not hurt, and this makes the proofs of atomicity simpler).

 19 Jul, 2016 1 commit


Robbert Krebbers authored

 15 Jul, 2016 1 commit


Robbert Krebbers authored

 13 Jul, 2016 1 commit


Robbert Krebbers authored
The intropattern {H} also meant clear (both in ssreflect, and the logic part of the introduction pattern).

 04 Jul, 2016 1 commit


JacquesHenri Jourdan authored

 30 Jun, 2016 2 commits


Ralf Jung authored
I know we don't use it. Stating theorems also serves to document things, and IMHO this one is informative. It also costs us nothing.

Robbert Krebbers authored
Concretely, when execution of any of the wp_ tactics does not yield another wp, it will make sure that a view shift is kept. This behavior was already partially there, but now it is hopefully more consistent.

 29 Jun, 2016 1 commit


Robbert Krebbers authored

 24 May, 2016 1 commit


Robbert Krebbers authored
Changes:  We no longer have a different syntax for specializing a term H : P ★ Q whose range P or domain Q is persistent. There is just one syntax, and the system automatically determines whether either P or Q is persistent.  While specializing a term, always modalities are automatically stripped. This gets rid of the specialization pattern !.  Make the syntax of specialization patterns more consistent. The syntax for generating a goal is [goal_spec] where goal_spec is one of the following: H1 .. Hn : generate a goal using hypotheses H1 .. Hn H1 .. Hn : generate a goal using all hypotheses but H1 .. Hn # : generate a goal for the premise in which all hypotheses can be used. This is only allowed when specializing H : P ★ Q where either P or Q is persistent. % : generate a goal for a pure premise.

 10 May, 2016 1 commit


Robbert Krebbers authored

 09 May, 2016 1 commit


Robbert Krebbers authored

 19 Apr, 2016 8 commits


Robbert Krebbers authored
This gets rid of the (ambiguous) notation %l, because we can declare LitLoc as a coercion. It also shortens the code.

Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored
That way, we do not have useless type annotations of the form "v : language.val heap_lang" cluttering about any goal. Note, that we could decide to eta expand everywhere (as we do for ∀ and ∃), and use the notation "WP e {{ Q }}" for "wp e ⊤ (λ _, Q)".

 07 Apr, 2016 1 commit


Robbert Krebbers authored

 30 Mar, 2016 1 commit


Ralf Jung authored
and show that this is an instance of evaluation contexts

 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

 15 Mar, 2016 1 commit


Ralf Jung authored

 12 Mar, 2016 1 commit


Ralf Jung authored

 10 Mar, 2016 3 commits


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 nonexpansive 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 userdefined 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 2 commits


Ralf Jung authored

Robbert Krebbers authored

 02 Mar, 2016 4 commits


Ralf Jung authored

Ralf Jung authored
get rid of substitution in Case (use lambdas); introduce Match as derived form that involves binders

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
This cleans up some adhoc 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.

 20 Feb, 2016 1 commit


Ralf Jung authored
