is there any project that sould convert coq proofs into another language than ML, even if that means making a few assumptions or using only a subset of the targ

is there any project that sould convert coq proofs into another language than ML, even if that means making a few assumptions or using only a subset of the target language ?