# \#extraction **URL:** https://discuss.ocaml.org/tag/extraction/642.md [Latest](https://discuss.ocaml.org/latest.md) · [Categories](https://discuss.ocaml.org/categories.md) · [Tags](https://discuss.ocaml.org/tags.md) --- ## [Calling extractable side-effect ocaml functions in Coq](https://discuss.ocaml.org/t/calling-extractable-side-effect-ocaml-functions-in-coq/13738)
**Author:** [@CharlesAverill](https://discuss.ocaml.org/u/CharlesAverill)\ **Replies:** 1\ **Last updated:** [December 30, 2023, 5:16pm UTC](https://discuss.ocaml.org/t/calling-extractable-side-effect-ocaml-functions-in-coq/13738 "2023-12-30T17:16:36Z")
I’d like to reason about Coq code that will eventually be extracted to OCaml. As a result, I’d like to be able to write Coq code that can generate side-effect OCaml code that calls functions like print\_endline. Digging …