- Sep 21, 2017
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Sep 20, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
In order to do that, we need to quantify over non-expansive 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
-
- Sep 19, 2017
- Sep 18, 2017
-
-
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
-
- Sep 17, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Sep 15, 2017
-
-
Robbert Krebbers authored
Fix typo in is_lock_proper for heap_lang. See merge request !57
-
- Sep 09, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Sep 08, 2017
-
-
Robbert Krebbers authored
-
- Sep 06, 2017
-
-
Robbert Krebbers authored
-
- Aug 28, 2017
-
-
Robbert Krebbers authored
persistent context. Given the source does not contain a box: - Before: no-op if there is a Persistent instance. - Now: no-op in all cases.
-
Robbert Krebbers authored
We now first iPoseProof the lemma and instantiate its premises before trying to search for the sub-term where to apply. As a result, instantiation of the premises of the applied lemmas happens only once, instead of it being done for each sub-term as obtained by reshape_expr.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Joshua Yanovski authored
-
Robbert Krebbers authored
- Use Φ and Ψ for predicates. - Use _1 and _2 suffixes for the different directions of a lemma. - Not all lemmas started with _uPred; we do not let the bigop lemmas (for instance) start with uPred_ either, so I just got rid of the prefix.
-
Robbert Krebbers authored
-