Данная статья является переводом моей статьи: Formalization of code in Coq - tactics , написанной в период работы над проектом coq-tezos-of-ocaml. Суть проекта: часть исходного кода протокола...