 25 Sep, 2017 13 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This problem has been reported by Léon Gondelman. Before, when using, for example wp_alloc, in an expression like: ref (ref v) It would apply `tac_wp_alloc` to the outermost ref, after which it fails to establish that the argument `ref v` is a value. In this commit, other evaluation positions will be tried whenever it turn out that the argument of the construct is not a value. The same applies to store/cas/... I have implemented this by making use of the new `IntoVal` class.

Dan Frumin authored

Dan Frumin authored
Expression `e` such that `to_val e = Some v` is in the context gets reflected into value `v` together with the proof that `to_val e = Some v`. This is helpful for substitution and for `solve_to_val` operating on the reflected syntax.

Dan Frumin authored

Dan Frumin authored
This way `IntoLaterNEnvs` is ought to be computed less frequently

Dan Frumin authored

Robbert Krebbers authored
The tactic was doing something weird and only once used.

Robbert Krebbers authored
 Get rid of wp_finish, which was a hack.  Write the wp_ tactics for stateful steps in the same style as wp_pure, i.e. by taking the context into account.  Make use of the context K in wp_pure.

Dan Frumin authored

Dan Frumin authored
Instead of writing a separate tactic lemma for each pure reduction, there is a single tactic lemma for performing all of them. The instances of PureExec can be shared between WP tactics and, e.g. symbolic execution in the ghost threadpool

Robbert Krebbers authored
Typeclass search gets less confused when this version is used, also, we had the same for `wp_bind` already.

 24 Sep, 2017 1 commit


Robbert Krebbers authored

 21 Sep, 2017 5 commits


Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored

 20 Sep, 2017 9 commits


Robbert Krebbers authored

Robbert Krebbers authored
In order to do that, we need to quantify over nonexpansive predicates instead of arbitrary predicates.

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored

 19 Sep, 2017 7 commits
 18 Sep, 2017 4 commits


Robbert Krebbers authored
That caused some problems, e.g.: From iris.base_logic Require Export fix. Gave: Syntax error: [constr:global] expected after [export_token] (in [vernac:gallina_ext]).

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

 17 Sep, 2017 1 commit


Robbert Krebbers authored
