"The compiler itself is also written in Scala and its underlying Coq parser is largely based on the use of parser combinators"

while "true" extractor has to be written in Coq, as I understand :-)