# MetaOCaml in Coq

**URL:** https://discourse.rocq-prover.org/t/metaocaml-in-coq/874
**Category:** Using Rocq
**Created:** [June 7, 2020, 11:56pm UTC](https://discourse.rocq-prover.org/t/metaocaml-in-coq/874 "2020-06-07T23:56:07Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![philzook58](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/philzook58/32/323_2.png) [@philzook58](https://discourse.rocq-prover.org/u/philzook58)
#### Post date: [June 7, 2020, 11:56pm UTC](https://discourse.rocq-prover.org/t/metaocaml-in-coq/874/1 "2020-06-07T23:56:07Z")

</div>

I’ve been thinking a bit about how to emulate MetaOCaml in Coq and was interested to see what people thought about it.

[https://www.philipzucker.com/metaocaml-style-partial-evaluation-in-coq/](https://www.philipzucker.com/metaocaml-style-partial-evaluation-in-coq/)

Suggestions welcome, thanks!