Job 3287

CakeML:6e2de3d9efb121902e22e7e3598f64820e434118
  Remove unnecessary local [Mar 25 07:49:27]
#1357 (noparse)
Merging into:4e312c0f7e18b9c5789c8ac4e0af257bff895cf5
  Define a C function for customFFI [Mar 25 03:52:57]
HOL:63f2eb9c146352dfd0bab8c5604a096d1e554d03
  minor fixes to examples and updated internal docs [Mar 17 21:01:43]