 26 Jun, 2016 1 commit


Robbert Krebbers authored
This is very experimental. It should now deal better with stuff like: match x with .. end = match y with .. end In case there is a hypothesis H : R x y, it will try to destruct it.

 31 May, 2016 3 commits


Ralf Jung authored

Robbert Krebbers authored

Robbert Krebbers authored
Now, for example, when having equiv (Some x) (Some y) it will try to find a Proper whose range is an equiv before hitting the eq instance. My hack is general enough that it works for Forall2, dist, and so on, too.

 11 Apr, 2016 1 commit


Robbert Krebbers authored

 10 Mar, 2016 1 commit


Robbert Krebbers authored
Thanks to Amin Timany for the suggestion.

 05 Mar, 2016 1 commit


Ralf Jung authored

 04 Mar, 2016 1 commit


Robbert Krebbers authored

 03 Mar, 2016 2 commits


Robbert Krebbers authored
Contrary to destruct_conj from Program.

Robbert Krebbers authored

 25 Feb, 2016 9 commits


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

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.

Ralf Jung authored

Ralf Jung authored

Robbert Krebbers authored

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

 24 Feb, 2016 1 commit


Ralf Jung authored

 23 Feb, 2016 1 commit


Ralf Jung authored

 22 Feb, 2016 1 commit


Robbert Krebbers authored

 20 Feb, 2016 1 commit


Ralf Jung authored

 19 Feb, 2016 1 commit


Robbert Krebbers authored

 17 Feb, 2016 4 commits


Robbert Krebbers authored

Robbert Krebbers authored
simplify_equality => simplify_eq simplify_equality' => simplify_eq/= simplify_map_equality => simplify_map_eq simplify_map_equality' => simplify_map_eq/= simplify_option_equality => simplify_option_eq simplify_list_equality => simplify_list_eq f_equal' => f_equal/= The /= suffixes (meaning: do simpl) are inspired by ssreflect.

Robbert Krebbers authored
The tactic injection H as H is doing exactly that.

Robbert Krebbers authored

 14 Feb, 2016 1 commit


Robbert Krebbers authored

 13 Feb, 2016 1 commit


Robbert Krebbers authored
Also, make our redefinition of done more robust under different orders of Importing modules.

 11 Feb, 2016 1 commit


Robbert Krebbers authored
Also do some minor clean up.

 08 Feb, 2016 1 commit


Robbert Krebbers authored

 02 Feb, 2016 1 commit


Ralf Jung authored

 18 Jan, 2016 1 commit


Robbert Krebbers authored

 16 Jan, 2016 1 commit


Robbert Krebbers authored

 12 Jan, 2016 1 commit


Robbert Krebbers authored

 17 Nov, 2015 1 commit


Robbert Krebbers authored

 16 Nov, 2015 1 commit


Robbert Krebbers authored

 11 Nov, 2015 1 commit


Robbert Krebbers authored
