Now we follow Coq's stdlib and declare this instance using a `Hint Extern`;
this avoids making `flip` type class opaque.

Revert "`RelDecision` instance for `flip`, and make `flip` tc opaque to avoid loops due to eager unification."

This reverts commit b81aa3aa.

`RelDecision` instance for `flip`, and make `flip` tc opaque to avoid loops due to eager unification.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

This allows for more control over `Hint Mode`.

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

This makes the typeclass mechanism able to use instances like [Is_true X -> Blah], where X reduces to X.

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.

Pointer equality is now defined using absolute object offsets. The treatment
is similar to CompCert:

* Equality of pointers in the same object is defined provided the object has
  not been deallocated.
* Equality of pointers in different objects is defined provided both pointers
  have not been deallocated and both are strict (i.e. not end-of-array).

Thus, pointer equality is defined for all pointers that are not-end-of-array
and have not been deallocated. The following examples have defined behavior:

  int x, y;
  printf("%d\n", &x == &y);
  int *p = malloc(sizeof(int)), *q = malloc(sizeof(int));
  printf("%d\n", p == q);
  struct S { int a; int b; } s, *r = &s;
  printf("%d\n", &s.a + 1 == &(r->b));

The following not:

  int x, y;
  printf("%d\n", &x + 1 == &y);

memory instead of the whole memory itself.

This has the following advantages:
* Avoid parametrization in {addresses,pointers,pointer_bits,bits}.v
* Make {base_values,values}.v independent of the memory, this makes better
  parallelized compilation possible.
* Allow small memories (e.g. singletons as used in separation logic) with
  addresses to objects in another part to be typed.
* Some proofs become easier, because the memory environments are preserved
  under many operations (insert, force, lock, unlock).

It also as the following disadvantages:
* At all kinds of places we now have explicit casts from memories to memory
  environments. This is kind of ugly. Note, we cannot declare memenv_of as a
  Coercion because it is non-uniform.
* It is a bit inefficient with respect to the interpreter, because memory
  environments are finite functions instead of proper functions, so calling
  memenv_of often (which we do) is not too good.

* Parametrize refinements with memories. This way, refinements imply typing,
  for example [w1 ⊑{Γ,f@m1↦m2} w2 : τ → (Γ,m1) ⊢ w1 : τ]. This relieves us from
  various hacks.
* Use addresses instead of index/references pairs for lookup and alter
  operations on memories.
* Prove various disjointness properties.

The refactoring includes:
* Use infix notations for the various list relations
* More consistent naming
* Put lemmas on one line whenever possible
* Change proofs into one-liners when possible
* Make better use of the "Implicit Types" command
* Improve the order of the list module by placing all definitions at the start,
  then the proofs, and finally the tactics.

Besides, there is some new machinery for proofs by reflection on lists. It is
used for a decision procedure for permutations and list containment.

Both the operational and axiomatic semantics are extended with sequence points
and a permission system based on fractional permissions. In order to achieve
this, the memory model has been completely revised, and is now built on top
of an abstract interface for permissions.

Apart from these changed, the library on lists and sets has been heavily
extended, and minor changed have been made to other parts of the prelude.

The development now corresponds exactly to the FoSSaCS 2013 paper.
Also, the prelude is updated to the one of the master branch.