GitLab

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.

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.

Contrary to destruct_conj from Program.

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

In principle, we could now un-seal 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.

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

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.

The tactic injection H as H is doing exactly that.

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

Also do some minor clean up.

The port makes the following notable changes:

* The carrier types of separation algebras and integer environments are no
  longer in Set. Now they have a type at a fixed type level above Set. This
  both works better in 8.5 and makes the formalization more general.
  I have tried putting them at polymorphic type levels, but that increased the
  compilation time by an order of magnitude.
* I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
  That bug has been fixed, so this custom tactic can be removed when the next
  beta of 8.5 is out.

The tactic "injection' H" now uses the name "H" for the first hypothesis it
generates. Fresh names will still be used for the remaining hypotheses.