 26 Feb, 2016 10 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
It now also contains a nonexpansiveness proof.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
I have simplified the following CMRA axioms: cmra_unit_preservingN n x y : x ≼{n} y → unit x ≼{n} unit y; cmra_op_minus n x y : x ≼{n} y → x ⋅ y ⩪ x ≡{n}≡ y; By dropping off the stepindex, so into: cmra_unit_preservingN x y : x ≼ y → unit x ≼ unit y; cmra_op_minus x y : x ≼ y → x ⋅ y ⩪ x ≡ y; The old axioms can be derived.

 25 Feb, 2016 27 commits


Ralf Jung authored

Ralf Jung authored
The changes are probably necessary because rewrite now tries harder not to instantiate evars, which it always said it would not do.

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored
It now turns setoid equalities into Leibniz equalities when possible, and substitutes those.

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Ralf Jung authored
In principle, we could now unseal heap_mapsto, saved_prop_own etc., and mark them as "Typeclass Opaque", and ecancel would still work just as fast as it does now. Thanks to Matthieu for pointing me to this unify feature.

Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored
Conflicts: prelude/tactics.v

Robbert Krebbers authored

Ralf Jung authored

Ralf Jung authored
This replaces f_equiv and solve_proper with our own, hopefully better, versions

Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored
The performance gain seems neglectable, unfortunatelly...

 24 Feb, 2016 3 commits


Robbert Krebbers authored
* Use sig instead of sigT: the proof is a Prop after all * Tweak implicit arguments * Shorten proof of sigma

Robbert Krebbers authored
It now traverses terms at most once, whereas the setoid_rewrite approach was travering terms many times. Also, the tactic can now be extended by defining type class instances.

Robbert Krebbers authored
