More work on memory alloc#733

clarus merged 4 commits intomainformal-land/coq-of-rust:mainfrom

guillaume-claret@simulate-stackformal-land/coq-of-rust:guillaume-claret@simulate-stackCopy head branch name to clipboard