Hiro Mizuno

I appreciate your help. I extract https://github.com/msgpack/msgpack-ocaml/blob/master/lib/core/msgpackCore.ml from Coq proof, and write other codes by hands.

To change internal representanion, Coq code should be changed, especially at extract config( https://github.com/msgpack/msgpack-ocaml/blob/master/proof/ExtractUtil.v).

Some methods of IMKCandidates don't work well. * [rdar://34944196: -\[IMKCandidates candidateStringIdentifier:\] always returns 0](https://openradar.appspot.com/34944196) * [rdar://34911503: -\[IMKCandidates showAnnotation:\] doesn't work](https://openradar.appspot.com/34911503)

IMK has some private features(and I want to use it) * [rdar://39295951: Add document: Keyboard Preferences pane](https://openradar.appspot.com/radar?id=5032263645396992) * [rdar://39296952: Add API & document: show keyboard layout for input methods](https://openradar.appspot.com/radar?id=4977705346924544) *...