Comment Comment by user2342 In case of coq-to-ocaml: is it feasible to do an extraction to OCaml on the translated code and compare it with the original? parent user2342 2 years ago