Coq/Rocq is a proof assistant written in O'Caml
