Merge branch 'master' into hacking

opam

theories/adequacy.v

theories/derived.v

theories/frac_borrow.v

theories/heap.v

theories/lang.v

theories/lft_contexts.v

theories/lifting.v

theories/memcpy.v

theories/perm.v

theories/perm_incl.v

theories/proofmode.v

theories/shr_borrow.v

theories/tl_borrow.v

theories/type.v

theories/type_incl.v

theories/typing.v