Discovered an extraction plugin for logical inductive relations in Coq
which are the type of the relation Ott produces for the reduction
relation. The original paper is at
http://cedric.cnam.fr/~delahaye/papers/pred-exec%20%28TPHOLs%2707%29.pdf

the repository is at 
https://github.com/picnic/RelationExtraction