I also changed the spec : this can be done even if the lifetime is not
ongoing, and thus it does not need tokens.

lifetime logic: use agree instead of dec_agree

If you are happy with this, we can merge this and <https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/22>

Cc @robbertkrebbers @jjourdan

See merge request !4

Also, to fix the build: use compatibility layer for ownP.
TODO : connect the heap invariant directly.

TODO : functions, sums. But these types need to be redefined properly.

Warning : splitting a own of a product only works if the list of types is non-empty.

Refactoring the type system : every type gets its own file. Some trivial ones are defined somewhere else where it make the most sense.

Coq 8.6

These are the changes necessary to make this compatible with Coq 8.6. Most of the changes are fine (and of the category "no idea why this worked in 8.5" or "the statement of a lemma changed in the 8.6 libs"), except for the horribleness in perm_incl.v. I played around a little but found no good way to restore the term into the state Coq 8.5 put it in -- and the goals I end up in otherwise (if I just remove the `change`) look fairly unsolvable.

Cc @jjourdan @robbertkrebbers

See merge request !3

This reverts commit 3ddb6014.
I did not intend to push this to master, sorry :/