MLCFG: allow arbitrary `let .. in ..` at the top of cfg function bodies
Currently the function bodies in MLCFG start with a block of local variable declarations under the form
var x : t;
var y : t';
...
This form is indeed a syntactic sugar for
let ref x = any t in
let ref y = any t' in
...
It is desirable to allow a more general form of local variable declarations, in particular to control in a more fine-grain way which data is mutable and which is not. The proposal would be to allow any WhyML let ... in ...
on top of CFG bodies