This branch is in a badly broken state. Even before the
merge, the build did no go through, as we did not finish
propagating the change to places in the semantic type
system to all files.

Nonetheless, the changes from master have now been merged,
with the exception of the following files:

theories/typing/lib/cell.v
theories/typing/soundness.v

(which require fixing other files before they can be compiled)

For these two files, the merge conflict has been commented out
and left in the file.